1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel, Yury Kudryashov
  5  -/
  6  
  7  import analysis.calculus.local_extr
src         └──────────────────────────┘
  8  import analysis.convex.topology
src         └──────────────────────┘
  9  
 10  /-!
 11  # The mean value inequality and equalities
 12  
 13  In this file we prove the following facts:
 14  
 15  * `convex.norm_image_sub_le_of_norm_deriv_le` : if `f` is differentaible on a convex set `s`
 16    and the norm of its derivative is bounded by `C`, then `f` is Lipschitz continuous on `s` with
 17    constant `C`.
 18  
 19  * `image_le_of*`, `image_norm_le_of_*` : several similar lemmas deducing `f x ≤ B x` or
 20    `∥f x∥ ≤ B x` from upper estimates on `f'` or `∥f'∥`, respectively. These lemmas differ by
 21    their assumptions:
 22  
 23    * `of_liminf_*` lemmas assume that limit inferior of some ratio is less than `B' x`;
 24    * `of_deriv_right_*`, `of_norm_deriv_right_*` lemmas assume that the right derivative
 25      or its norm is less than `B' x`;
 26    * `of_*_lt_*` lemmas assume a strict inequality whenever `f x = B x` or `∥f x∥ = B x`;
 27    * `of_*_le_*` lemmas assume a non-strict inequality everywhere on `[a, b)`;
 28    * name of a lemma ends with `'` if (1) it assumes that `B` is continuous on `[a, b]`
 29      and has a right derivative at every point of `[a, b)`, and (2) the lemma has
 30      a counterpart assuming that `B` is differentiable everywhere on `ℝ`
 31  
 32  * `norm_image_sub_le_*_segment` : if derivative of `f` on `[a, b]` is bounded above
 33    by a constant `C`, then `∥f x - f a∥ ≤ C * ∥x - a∥`; several versions deal with
 34    right derivative and derivative within `[a, b]` (`has_deriv_within_at` or `deriv_within`).
 35  
 36  * `convex.is_const_of_fderiv_within_eq_zero` : if a function has derivative `0` on a convex set `s`,
 37    then it is a constant on `s`.
 38  
 39  * `exists_ratio_has_deriv_at_eq_ratio_slope` and `exists_ratio_deriv_eq_ratio_slope` :
 40    Cauchy's Mean Value Theorem.
 41  
 42  * `exists_has_deriv_at_eq_slope` and `exists_deriv_eq_slope` : Lagrange's Mean Value Theorem.
 43  
 44  * `convex.image_sub_lt_mul_sub_of_deriv_lt`, `convex.mul_sub_lt_image_sub_of_lt_deriv`,
 45    `convex.image_sub_le_mul_sub_of_deriv_le`, `convex.mul_sub_le_image_sub_of_le_deriv`,
 46    if `∀ x, C (</≤/>/≥) (f' x)`, then `C * (y - x) (</≤/>/≥) (f y - f x)` whenever `x < y`.
 47  
 48  * `convex.mono_of_deriv_nonneg`, `convex.antimono_of_deriv_nonpos`,
 49    `convex.strict_mono_of_deriv_pos`, `convex.strict_antimono_of_deriv_neg` :
 50    if the derivative of a function is non-negative/non-positive/positive/negative, then
 51    the function is monotone/monotonically decreasing/strictly monotone/strictly monotonically
 52    decreasing.
 53  
 54  * `convex_on_of_deriv_mono`, `convex_on_of_deriv2_nonneg` : if the derivative of a function
 55    is increasing or its second derivative is nonnegative, then the original function is convex.
 56  -/
 57  
 58  set_option class.instance_max_depth 120
doc             └──────────────────────┘
 59  
 60  variables {E : Type*} [normed_group E] [normed_space ℝ E]
id                          └──────────┘     └──────────┘ 
src                         └──────────┘     └──────────┘ 
typ                         └──────────┘     └──────────┘ 
doc                         └──────────┘     └──────────┘
 61            {F : Type*} [normed_group F] [normed_space ℝ F]
id                          └──────────┘     └──────────┘ 
src                         └──────────┘     └──────────┘ 
typ                         └──────────┘     └──────────┘ 
doc                         └──────────┘     └──────────┘
 62  
 63  open metric set lattice asymptotics continuous_linear_map filter
 64  open_locale classical topological_space
 65  
 66  /-! ### One-dimensional fencing inequalities -/
 67  
 68  /-- General fencing theorem for continuous functions with an estimate on the derivative.
 69  Let `f` and `B` be continuous functions on `[a, b]` such that
 70  
 71  * `f a ≤ B a`;
 72  * `B` has right derivative `B'` at every point of `[a, b)`;
 73  * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
 74    is bounded above by a function `f'`;
 75  * we have `f' x < B' x` whenever `f x = B x`.
 76  
 77  Then `f x ≤ B x` everywhere on `[a, b]`. -/
 78  lemma image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ}
id                                                                               
src                                                                              
typ                                                                              
 79    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
 80    -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x`
 81    (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id                 └─┘        └┘   
src                └─┘                
typ                └─┘        └┘   
doc                 └─┘
 82      ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r)
id       └┘  └┘ └─────────┘   └─┘       └┘          
src      └┘   └┘ └─────────┘    └─┘          └┘             
typ      └┘  └┘ └─────────┘   └─┘       └┘          
doc      └┘   └┘ └─────────┘    └─┘   
 83    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                          └───────────┘    └─┘
 84    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
 85    (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
 86    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
 87  begin
st   └─────
 88    change Icc a b ⊆ {x | f x ≤ B x},
id            └─┘             
src    └─────┘└─┘  └──┘     
typ    └─────┘└─┘└──┘   
doc    └─────┘└─┘    └──┘     
txt    └─────┘       └──┘     
par    └─────┘       └──┘     
pid                 └──┘     
st   ─────────────────────────────────┘└─
 89    set s := {x | f x ≤ B x} ∩ Icc a b,
id                            └─┘  
src    └───────┘ └──┘    └┘└─┘ 
typ    └───────┘ └──┘  └┘└─┘
doc    └───────┘ └──┘     └┘ └─┘ 
txt    └───────┘ └──┘     └┘     
par    └───────┘ └──┘     └┘     
pid       └┘ └──┘     └┘     
st   ───────────────────────────────────┘└─
 90    have A : continuous_on (λ x, (f x, B x)) (Icc a b), from hf.prod hB,
id              └───────────┘                 └─┘          └─────┘ └┘
src    └───────┘└───────────┘  └──┘  └┘  └─┘ └─┘    └───┘└─────┘
typ    └───────┘└───────────┘  └──┘ └┘ └─┘ └─┘  └───┘└─────┘└┘
doc    └───────┘└───────────┘  └──┘   └┘  └─┘ └─┘    └───┘       
txt    └───────┘               └──┘   └┘  └─┘        └───┘       
par    └───────┘               └──┘   └┘  └─┘        └───┘       
pid    └────┘└─┘               └──┘   └┘  └─┘        └───┘       
st   ───────────────────────────────────────────────────┘└───────────────┘└─
 91    have : is_closed s,
id            └───────┘ 
src    └─────┘└───────┘
typ    └─────┘└───────┘
doc    └─────┘└───────┘
txt    └─────┘         
par    └─────┘         
pid    └───┘└┘         
st   ───────────────────┘└─
 92    { simp only [s, inter_comm],
id                    └────────┘
src      └─────────┘ └┘└────────┘
typ      └─────────┘└┘└────────┘
doc      └─────────┘ └┘          
txt      └─────────┘ └┘          
par      └─────────┘ └┘          
pid          └──┘└┘ └┘          
st   ───┘└───────────────────────┘└─
 93      exact A.preimage_closed_of_closed is_closed_Icc (order_closed_topology.is_closed_le' _) },
id             └─────────────────────────┘ └───────────┘  └─────────────────────────────────┘
src      └────┘└─────────────────────────┘└───────────┘ └─────────────────────────────────┘└──┘
typ      └────┘└─────────────────────────┘└───────────┘ └─────────────────────────────────┘└──┘
doc      └────┘                                                                            └──┘
txt      └────┘                                                                            └──┘
par      └────┘                                                                            └──┘
pid                                                                                       └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└┘
 94    apply this.Icc_subset_of_forall_exists_gt ha,
id           └─────────────────────────────────┘ └┘
src    └────┘└─────────────────────────────────┘
typ    └────┘└─────────────────────────────────┘└┘
doc    └────┘└─────────────────────────────────┘
txt    └────┘                                   
par    └────┘                                   
pid                                            
st   ─────────────────────────────────────────────┘└─
 95    rintros x ⟨hxB, xab⟩ y hy,
src    └───────────────────────┘
typ    └───────────────────────┘
doc    └───────────────────────┘
txt    └───────────────────────┘
par    └───────────────────────┘
pid           └────────────────┘
st   ──────────────────────────┘└─
 96    change f x ≤ B x at hxB,
id                  
src    └─────┘     └─────┘
typ    └─────┘  └─────┘
doc    └─────┘     └─────┘
txt    └─────┘     └─────┘
par    └─────┘     └─────┘
pid               └────┘
st   ────────────────────────┘└─
 97    cases lt_or_eq_of_le hxB with hxB hxB,
id           └────────────┘ └─┘
src    └────┘└────────────┘   └───────────┘
typ    └────┘└────────────┘└─┘└───────────┘
doc    └────┘                 └───────────┘
txt    └────┘                 └───────────┘
par    └────┘                 └───────────┘
pid                          └───────────┘
st   ──────────────────────────────────────┘└─
 98    { -- If `f x < B x`, then all we need is continuity of both sides
st   ───┘└───────────────────────────────────────────────────────────────
 99      apply nonempty_of_mem_sets (nhds_within_Ioi_self_ne_bot x),
id             └──────────────────┘  └─────────────────────────┘ 
src      └────┘└──────────────────┘ └─────────────────────────┘ 
typ      └────┘└──────────────────┘ └─────────────────────────┘
doc      └────┘                                                 
txt      └────┘                                                 
par      └────┘                                                 
pid                                                            
st   ─────────────────────────────────────────────────────────────┘└─
100      refine inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_refl x, hy⟩),
id              └────────────┘    └─────────────────────┘  └─────┘   └┘
src      └─────┘└────────────┘└─┘ └─────────────────────┘ └─────┘ └┘  └┘
typ      └─────┘└────────────┘└─┘ └─────────────────────┘ └─────┘└┘└┘└┘
doc      └─────┘              └─┘                                 └┘  └┘
txt      └─────┘              └─┘                                 └┘  └┘
par      └─────┘              └─┘                                 └┘  └┘
pid                          └─┘                                 └┘  └┘
st   ────────────────────────────────────────────────────────────────────┘└─
101      have : ∀ᶠ x in nhds_within x (Icc a b), f x < B x,
id              └┘   └┘ └─────────┘   └─┘        
src      └─────┘└┘└─┘└┘└─────────┘  └─┘     
typ      └─────┘└┘└─┘└┘└─────────┘ └─┘ 
doc      └─────┘└┘└─┘└┘└─────────┘  └─┘      
txt      └─────┘  └─┘                         
par      └─────┘  └─┘                         
pid      └───┘└┘  └─┘                         
st   ────────────────────────────────────────────────────┘└─
102        from A x (Ico_subset_Icc_self xab)
id                 └─────────────────┘ └─┘
src        └───┘   └─────────────────┘   └─
typ        └───┘ └─────────────────┘└─┘└─
doc        └───┘                         └─
txt        └───┘                         └─
par        └───┘                         └─
pid        └───┘                         └─
st   ─────────────────────────────────────────
103          (mem_nhds_sets (is_open_lt continuous_fst continuous_snd) hxB),
id            └───────────┘  └────────┘ └────────────┘ └────────────┘  └─┘
src  ───────┘ └───────────┘ └────────┘└────────────┘└────────────┘└┘   
typ  ───────┘ └───────────┘ └────────┘└────────────┘└────────────┘└┘└─┘
doc  ───────┘                                                     └┘   
txt  ───────┘                                                     └┘   
par  ───────┘                                                     └┘   
pid  ───────┘                                                     └┘   
st   ─────────────────────────────────────────────────────────────────────┘└─
104      have : ∀ᶠ x in nhds_within x (Ioi x), f x < B x,
id              └┘   └┘ └─────────┘    └─┘        
src      └─────┘└┘└─┘└┘└─────────┘  └─┘     
typ      └─────┘└┘└─┘└┘└─────────┘  └─┘  
doc      └─────┘└┘└─┘└┘└─────────┘  └─┘     
txt      └─────┘  └─┘                        
par      └─────┘  └─┘                        
pid      └───┘└┘  └─┘                        
st   ──────────────────────────────┘└─────────────────┘└─
105        from nhds_within_le_of_mem (Icc_mem_nhds_within_Ioi xab) this,
id              └───────────────────┘  └─────────────────────┘ └─┘  └──┘
src        └───┘└───────────────────┘ └─────────────────────┘   └┘
typ        └───┘└───────────────────┘ └─────────────────────┘└─┘└┘└──┘
doc        └───┘                                                └┘
txt        └───┘                                                └┘
par        └───┘                                                └┘
pid        └───┘                                                └┘
st   ──────────────────────────────────────────────────────────────────┘└─
106      refine mem_sets_of_superset this (set_of_subset_set_of.2 $ λ y, le_of_lt) },
id              └──────────────────┘ └──┘  └──────────────────┘          └──────┘
src      └─────┘└──────────────────┘     └──────────────────┘└─┘  └──┘└──────┘└┘
typ      └─────┘└──────────────────┘└──┘ └──────────────────┘└─┘  └──┘└──────┘└┘
doc      └─────┘                                             └─┘  └──┘        └┘
txt      └─────┘                                             └─┘  └──┘        └┘
par      └─────┘                                             └─┘  └──┘        └┘
pid                                                         └─┘  └──┘        
st   ─────────────────────────────────────────────────────────────────────────────┘└┘
107    { rcases dense (bound x xab hxB) with ⟨r, hfr, hrB⟩,
id              └───┘  └───┘  └─┘ └─┘
src      └─────┘└───┘             └──────────────────┘
typ      └─────┘└───┘ └───┘└─┘└─┘└──────────────────┘
doc      └─────┘                  └──────────────────┘
txt      └─────┘                  └──────────────────┘
par      └─────┘                  └──────────────────┘
pid                              └──────────────────┘
st   ────────────────────────────────────────────────────┘└─
108      specialize hf' x xab r hfr,
id                  └─┘  └─┘  └─┘
src      └─────────┘        
typ      └─────────┘└─┘└─┘└─┘
doc      └─────────┘        
txt      └─────────┘        
par      └─────────┘        
pid                        
st   ─────────────────────────────┘└─
109      have HB : ∀ᶠ z in nhds_within x (Ioi x), r < (z - x)⁻¹ * (B z - B x),
id                 └┘   └┘ └─────────┘    └─┘            └┘         
src      └────────┘└┘└─┘└┘└─────────┘  └─┘      └┘      
typ      └────────┘└┘└─┘└┘└─────────┘  └─┘    └┘     
doc      └────────┘└┘└─┘└┘└─────────┘  └─┘                
txt      └────────┘  └─┘                                   
par      └────────┘  └─┘                                   
pid      └─────┘└─┘  └─┘                                   
st   ───────────────────────────────────────────────────────────────────────┘└─
110        from (has_deriv_within_at_iff_tendsto_slope' $ lt_irrefl x).1 (hB' x xab)
id               └────────────────────────────────────┘   └───────┘       └─┘  └─┘
src        └───┘ └────────────────────────────────────┘ └───────┘ └──┘        └─
typ        └───┘ └────────────────────────────────────┘ └───────┘ └──┘ └─┘└─┘└─
doc        └───┘                                                  └──┘        └─
txt        └───┘                                                  └──┘        └─
par        └───┘                                                  └──┘        └─
pid        └───┘                                                  └──┘        └─
st   ────────────────────────────────────────────────────────────────────────────────
111          (mem_nhds_sets is_open_Ioi hrB),
id            └───────────┘ └─────────┘ └─┘
src  ───────┘ └───────────┘└─────────┘   
typ  ───────┘ └───────────┘└─────────┘└─┘
doc  ───────┘                            
txt  ───────┘                            
par  ───────┘                            
pid  ───────┘                            
st   ──────────────────────────────────────┘└─
112      obtain ⟨z, ⟨hfz, hzB⟩, hz⟩ :
src      └────────────────────────────
typ      └────────────────────────────
doc      └────────────────────────────
txt      └────────────────────────────
par      └────────────────────────────
pid            └──────────────────────
st   ─────────────────────────────────
113        ∃ z, ((z - x)⁻¹ * (f z - f x) < r ∧ r < (z - x)⁻¹ * (B z - B x)) ∧ z ∈ Ioc x y,
id                                                                          └─┘  
src  ─────┘└┘              └┘                  └─┘  └─┘ 
typ  ─────┘└┘             └┘                └─┘  └─┘
doc  ─────┘ └┘               └┘                  └─┘   └─┘ 
txt  ─────┘ └┘               └┘                  └─┘       
par  ─────┘ └┘               └┘                  └─┘       
pid  ─────┘ └┘               └┘                  └─┘       
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
114        from ((hf'.and_eventually HB).and_eventually
id                └────────────────┘ └┘
src        └───┘  └────────────────┘  └────────────────
typ        └───┘  └────────────────┘└┘└────────────────
doc        └───┘                      └────────────────
txt        └───┘                      └────────────────
par        └───┘                      └────────────────
pid        └───┘                      └────────────────
st   ───────────────────────────────────────────────────
115          (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hy⟩)).exists,
id            └─────────────────────┘  └─────┘    └┘
src  ───────┘ └─────────────────────┘ └─────┘└──┘  └────────┘
typ  ───────┘ └─────────────────────┘ └─────┘└──┘└┘└────────┘
doc  ───────┘                                └──┘  └────────┘
txt  ───────┘                                └──┘  └────────┘
par  ───────┘                                └──┘  └────────┘
pid  ───────┘                                └──┘  └───────┘
st   ────────────────────────────────────────────────────────┘└─
116      have := le_of_lt (lt_trans hfz hzB),
id               └──────┘  └──────┘ └─┘ └─┘
src      └──────┘└──────┘ └──────┘      
typ      └──────┘└──────┘ └──────┘└─┘└─┘
doc      └──────┘                       
txt      └──────┘                       
par      └──────┘                       
pid      └───┘└─┘                       
st   ──────────────────────────────────────┘└─
117      refine ⟨z, _, hz⟩,
id                    └┘
src      └─────┘  └───┘  
typ      └─────┘ └───┘└┘
doc      └─────┘  └───┘  
txt      └─────┘  └───┘  
par      └─────┘  └───┘  
pid              └───┘  
st   ────────────────────┘└─
118      rw [mul_le_mul_left (inv_pos $ sub_pos.2 hz.1), hxB, sub_le_sub_iff_right] at this,
id           └─────────────┘  └─────┘   └─────┘   └┘     └─┘  └──────────────────┘
src      └──┘└─────────────┘ └─────┘ └─────┘└─┘  └───┘   └┘└──────────────────┘└───────┘
typ      └──┘└─────────────┘ └─────┘ └─────┘└─┘└┘└───┘└─┘└┘└──────────────────┘└───────┘
doc      └──┘                               └─┘  └───┘   └┘                    └───────┘
txt      └──┘                               └─┘  └───┘   └┘                    └───────┘
par      └──┘                               └─┘  └───┘   └┘                    └───────┘
pid        └┘                               └─┘  └───┘   └┘                    └──────┘
st   ─────────────────────────────────────────────────┘└───┘└────────────────────┘└──────┘└─
119      exact this }
id             └──┘
src      └────┘    
typ      └────┘└──┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ──────────────┘└─
120  end
st   ──┘
121  
122  /-- General fencing theorem for continuous functions with an estimate on the derivative.
123  Let `f` and `B` be continuous functions on `[a, b]` such that
124  
125  * `f a ≤ B a`;
126  * `B` has derivative `B'` everywhere on `ℝ`;
127  * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
128    is bounded above by a function `f'`;
129  * we have `f' x < B' x` whenever `f x = B x`.
130  
131  Then `f x ≤ B x` everywhere on `[a, b]`. -/
132  lemma image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id                                                                              
src                                                                             
typ                                                                             
133    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
134    -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x`
135    (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id                 └─┘        └┘   
src                 └─┘                
typ                └─┘        └┘   
doc                 └─┘
136      ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r)
id       └┘  └┘ └─────────┘   └─┘       └┘          
src      └┘   └┘ └─────────┘    └─┘          └┘             
typ      └┘  └┘ └─────────┘   └─┘       └┘          
doc      └┘   └┘ └─────────┘    └─┘   
137    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id                                        └──────────┘   └┘   
src                                            └──────────┘
typ                                       └──────────┘   └┘   
doc                                               └──────────┘
138    (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
139    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
140  image_le_of_liminf_slope_right_lt_deriv_boundary' hf hf' ha
id   └───────────────────────────────────────────────┘ └┘ └─┘ └┘
src  └───────────────────────────────────────────────┘
typ  └───────────────────────────────────────────────┘ └┘ └─┘ └┘
doc  └───────────────────────────────────────────────┘
141    (λ x hx, (hB x).continuous_at.continuous_within_at)
id         └┘   └┘  └───────────┘ └──────────────────┘
src                   └───────────┘ └──────────────────┘
typ        └┘   └┘  └───────────┘ └──────────────────┘
142    (λ x hx, (hB x).has_deriv_within_at) bound
id         └┘   └┘  └─────────────────┘   └───┘
src                   └─────────────────┘
typ        └┘   └┘  └─────────────────┘   └───┘
143  
144  /-- General fencing theorem for continuous functions with an estimate on the derivative.
145  Let `f` and `B` be continuous functions on `[a, b]` such that
146  
147  * `f a ≤ B a`;
148  * `B` has right derivative `B'` at every point of `[a, b)`;
149  * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
150    is bounded above by `B'`.
151  
152  Then `f x ≤ B x` everywhere on `[a, b]`. -/
153  lemma image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ}
id                                                                           
src                                                                          
typ                                                                          
154    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
155    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                          └───────────┘    └─┘
156    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
157    -- `bound` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ B' x`
158    (bound : ∀ x ∈ Ico a b, ∀ r, B' x < r →
id                   └─┘        └┘   
src                   └─┘                
typ                  └─┘        └┘   
doc                   └─┘
159      ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) :
id       └┘  └┘ └─────────┘   └─┘       └┘          
src      └┘   └┘ └─────────┘    └─┘          └┘             
typ      └┘  └┘ └─────────┘   └─┘       └┘          
doc      └┘   └┘ └─────────┘    └─┘   
160    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
161  begin
st   └─────
162    have Hr : ∀ x ∈ Icc a b, ∀ r ∈ Ioi (0:ℝ), f x ≤ B x + r * (x - a),
id                     └─┘           └─┘                       
src    └────────┘ └───┘└─┘    └───┘└─┘ └┘          
typ    └────────┘ └───┘└─┘   └───┘└─┘ └┘       
doc    └────────┘ └───┘└─┘    └───┘└─┘ └┘              
txt    └────────┘ └───┘       └───┘    └┘              
par    └────────┘ └───┘       └───┘    └┘              
pid    └─────┘└─┘ └───┘       └───┘    └┘              
st   ──────────────────────────────────────────────────────────────────┘└─
163    { intros x hx r hr,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───┘└──────────────┘└─
164      apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound,
id             └───────────────────────────────────────────────┘ └┘ └───┘
src      └────┘└───────────────────────────────────────────────┘  
typ      └────┘└───────────────────────────────────────────────┘└┘└───┘
doc      └────┘└───────────────────────────────────────────────┘  
txt      └────┘                                                   
par      └────┘                                                   
pid                                                              
st   ───────────────────────────────────────────────────────────────────┘└─
165      { rwa [sub_self, mul_zero, add_zero] },
id              └──────┘  └──────┘  └──────┘
src        └───┘└──────┘└┘└──────┘└┘└──────┘└┘
typ        └───┘└──────┘└┘└──────┘└┘└──────┘└┘
doc        └───┘        └┘        └┘        └┘
txt        └───┘        └┘        └┘        └┘
par        └───┘        └┘        └┘        └┘
pid           └┘        └┘        └┘        
st   ─────┘└───────────┘└────────┘└────────┘└┘
166      { exact hB.add (continuous_on_const.mul
id               └────┘  └─────────────────────┘
src        └────┘└────┘ └─────────────────────┘
typ        └────┘└────┘ └─────────────────────┘
doc        └────┘                              
txt        └────┘                              
par        └────┘                              
pid                                           
st   ─────┘└─────────────────────────────────────
167          (continuous_id.continuous_on.sub continuous_on_const)) },
id            └─────────────────────────────┘ └─────────────────┘
src  ───────┘ └─────────────────────────────┘└─────────────────┘└─┘
typ  ───────┘ └─────────────────────────────┘└─────────────────┘└─┘
doc  ───────┘                                                   └─┘
txt  ───────┘                                                   └─┘
par  ───────┘                                                   └─┘
pid  ───────┘                                                   └┘
st   ──────────────────────────────────────────────────────────────┘└┘
168      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
169        exact (hB' x hx).add (((has_deriv_within_at_id x (Ioi x)).sub_const a).const_mul r) },
id                └─┘   └┘         └────────────────────┘    └─┘                          
src        └────┘       └────┘   └────────────────────┘  └─┘ └───────────┘ └──────────┘ └┘
typ        └────┘ └─┘ └┘└────┘   └────────────────────┘  └─┘└───────────┘└──────────┘└┘
doc        └────┘       └────┘                           └─┘ └───────────┘ └──────────┘ └┘
txt        └────┘       └────┘                               └───────────┘ └──────────┘ └┘
par        └────┘       └────┘                               └───────────┘ └──────────┘ └┘
pid                    └────┘                               └───────────┘ └──────────┘ 
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└┘
170      { assume x hx _,
src        └───────────┘
typ        └───────────┘
doc        └───────────┘
txt        └───────────┘
par        └───────────┘
pid        └───────────┘
st   ─────┘└───────────┘└─
171        rw [mul_one],
id             └─────┘
src        └──┘└─────┘
typ        └──┘└─────┘
doc        └──┘       
txt        └──┘       
par        └──┘       
pid          └┘       
st   ────────────────┘└──
172        exact (lt_add_iff_pos_right _).2 hr },
id                └──────────────────┘      └┘
src        └────┘ └──────────────────┘└────┘  
typ        └────┘ └──────────────────┘└────┘└┘
doc        └────┘                     └────┘  
txt        └────┘                     └────┘  
par        └────┘                     └────┘  
pid                                  └────┘  
st   ─────────────────────────────────────────┘└┘
173      exact hx },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ────────────┘└┘
174    assume x hx,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
175    have : continuous_within_at (λ r, B x + r * (x - a)) (Ioi 0) 0,
id            └──────────────────┘                        └─┘
src    └─────┘└──────────────────┘  └──┘         └─┘ └─┘└───┘
typ    └─────┘└──────────────────┘  └──┘      └─┘ └─┘└───┘
doc    └─────┘└──────────────────┘  └──┘         └─┘ └─┘└───┘
txt    └─────┘                      └──┘         └─┘    └───┘
par    └─────┘                      └──┘         └─┘    └───┘
pid    └───┘└┘                      └──┘         └─┘    └──┘
st   ───────────────────────────────────────────────────────────────┘└─
176      from continuous_within_at_const.add (continuous_within_at_id.mul continuous_within_at_const),
id            └────────────────────────────┘  └─────────────────────────┘ └────────────────────────┘
src      └───┘└────────────────────────────┘ └─────────────────────────┘└────────────────────────┘
typ      └───┘└────────────────────────────┘ └─────────────────────────┘└────────────────────────┘
doc      └───┘                                                                                    
txt      └───┘                                                                                    
par      └───┘                                                                                    
pid      └───┘                                                                                    
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
177    convert continuous_within_at_const.closure_le _ this (Hr x hx); simp [closure_Ioi]
id             └───────────────────────────────────┘   └──┘  └┘  └┘         └─────────┘
src    └──────┘└───────────────────────────────────┘└─┘            └────┘└─────────┘└┘
typ    └──────┘└───────────────────────────────────┘└─┘└──┘ └┘└┘  └────┘└─────────┘└┘
doc    └──────┘                                     └─┘            └────┘└─────────┘└┘
txt    └──────┘                                     └─┘            └────┘           └┘
par    └──────┘                                     └─┘            └────┘           └┘
pid                                                └─┘                           
st   ────────────────────────────────────────────────────────────────────────────────────┘
178  end
st   └─┘
179  
180  /-- General fencing theorem for continuous functions with an estimate on the derivative.
181  Let `f` and `B` be continuous functions on `[a, b]` such that
182  
183  * `f a ≤ B a`;
184  * `B` has right derivative `B'` at every point of `[a, b)`;
185  * `f` has right derivative `f'` at every point of `[a, b)`;
186  * we have `f' x < B' x` whenever `f x = B x`.
187  
188  Then `f x ≤ B x` everywhere on `[a, b]`. -/
189  lemma image_le_of_deriv_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ}
id                                                                        
src                                                                       
typ                                                                       
190    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
191    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
192    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                          └───────────┘    └─┘
193    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
194    (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
195    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
196  image_le_of_liminf_slope_right_lt_deriv_boundary' hf
id   └───────────────────────────────────────────────┘ └┘
src  └───────────────────────────────────────────────┘
typ  └───────────────────────────────────────────────┘ └┘
doc  └───────────────────────────────────────────────┘
197    (λ x hx r hr, (hf' x hx).liminf_right_slope_le hr) ha hB hB' bound
id         └┘  └┘   └─┘  └┘ └───────────────────┘  └┘  └┘ └┘ └─┘ └───┘
src                            └───────────────────┘
typ        └┘  └┘   └─┘  └┘ └───────────────────┘  └┘  └┘ └┘ └─┘ └───┘
198  
199  /-- General fencing theorem for continuous functions with an estimate on the derivative.
200  Let `f` and `B` be continuous functions on `[a, b]` such that
201  
202  * `f a ≤ B a`;
203  * `B` has derivative `B'` everywhere on `ℝ`;
204  * `f` has right derivative `f'` at every point of `[a, b)`;
205  * we have `f' x < B' x` whenever `f x = B x`.
206  
207  Then `f x ≤ B x` everywhere on `[a, b]`. -/
208  lemma image_le_of_deriv_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id                                                                       
src                                                                      
typ                                                                      
209    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
210    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
211    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id                                        └──────────┘   └┘   
src                                            └──────────┘
typ                                       └──────────┘   └┘   
doc                                               └──────────┘
212    (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
213    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
214  image_le_of_deriv_right_lt_deriv_boundary' hf hf' ha
id   └────────────────────────────────────────┘ └┘ └─┘ └┘
src  └────────────────────────────────────────┘
typ  └────────────────────────────────────────┘ └┘ └─┘ └┘
doc  └────────────────────────────────────────┘
215    (λ x hx, (hB x).continuous_at.continuous_within_at)
id         └┘   └┘  └───────────┘ └──────────────────┘
src                   └───────────┘ └──────────────────┘
typ        └┘   └┘  └───────────┘ └──────────────────┘
216    (λ x hx, (hB x).has_deriv_within_at) bound
id         └┘   └┘  └─────────────────┘   └───┘
src                   └─────────────────┘
typ        └┘   └┘  └─────────────────┘   └───┘
217  
218  /-- General fencing theorem for continuous functions with an estimate on the derivative.
219  Let `f` and `B` be continuous functions on `[a, b]` such that
220  
221  * `f a ≤ B a`;
222  * `B` has derivative `B'` everywhere on `ℝ`;
223  * `f` has right derivative `f'` at every point of `[a, b)`;
224  * we have `f' x ≤ B' x` on `[a, b)`.
225  
226  Then `f x ≤ B x` everywhere on `[a, b]`. -/
227  lemma image_le_of_deriv_right_le_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id                                                                       
src                                                                      
typ                                                                      
228    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
229    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
230    {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                          └───────────┘    └─┘
231    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
232    (bound : ∀ x ∈ Ico a b, f' x ≤ B' x) :
id                   └─┘    └┘   └┘ 
src                   └─┘           
typ                  └─┘    └┘   └┘ 
doc                   └─┘
233    ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
234  image_le_of_liminf_slope_right_le_deriv_boundary hf ha hB hB' $
id   └──────────────────────────────────────────────┘ └┘ └┘ └┘ └─┘
src  └──────────────────────────────────────────────┘
typ  └──────────────────────────────────────────────┘ └┘ └┘ └┘ └─┘
doc  └──────────────────────────────────────────────┘
235  assume x hx r hr, (hf' x hx).liminf_right_slope_le (lt_of_le_of_lt (bound x hx) hr)
id           └┘  └┘   └─┘  └┘ └───────────────────┘   └────────────┘  └───┘  └┘  └┘
src                              └───────────────────┘   └────────────┘
typ          └┘  └┘   └─┘  └┘ └───────────────────┘   └────────────┘  └───┘  └┘  └┘
236  
237  /-! ### Vector-valued functions `f : ℝ → E` -/
238  
239  section
240  
241  variables {f : ℝ → E} {a b : ℝ}
id                               
src                              
typ                              
242  
243  /-- General fencing theorem for continuous functions with an estimate on the derivative.
244  Let `f` and `B` be continuous functions on `[a, b]` such that
245  
246  * `∥f a∥ ≤ B a`;
247  * `B` has right derivative at every point of `[a, b)`;
248  * for each `x ∈ [a, b)` the right-side limit inferior of `(∥f z∥ - ∥f x∥) / (z - x)`
249    is bounded above by a function `f'`;
250  * we have `f' x < B' x` whenever `∥f x∥ = B x`.
251  
252  Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. -/
253  lemma image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {E : Type*} [normed_group E]
id                                                                                 └──────────┘ 
src                                                                                └──────────┘
typ                                                                                └──────────┘ 
doc                                                                                └──────────┘
254    {f : ℝ → E} {f' : ℝ → ℝ} (hf : continuous_on f (Icc a b))
id                                └───────────┘   └─┘  
src                                └───────────┘    └─┘
typ                               └───────────┘   └─┘  
doc                                   └───────────┘    └─┘
255    -- `hf'` actually says `liminf ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) ≤ f' x`
256    (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id                 └─┘        └┘   
src                 └─┘                
typ                └─┘        └┘   
doc                 └─┘
257      ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r)
id       └┘  └┘ └─────────┘   └─┘       └┘          
src      └┘   └┘ └─────────┘    └─┘          └┘             
typ      └┘  └┘ └─────────┘   └─┘       └┘          
doc      └┘   └┘ └─────────┘    └─┘   
258    {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                            └───────────┘    └─┘
259    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
260    (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → f' x < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
261    ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
262  image_le_of_liminf_slope_right_lt_deriv_boundary' (continuous_norm.comp_continuous_on hf) hf'
id   └───────────────────────────────────────────────┘  └─────────────┘└─────────────────┘ └┘  └─┘
src  └───────────────────────────────────────────────┘  └─────────────┘└─────────────────┘
typ  └───────────────────────────────────────────────┘  └─────────────┘└─────────────────┘ └┘  └─┘
doc  └───────────────────────────────────────────────┘
263      ha hB hB' bound
id       └┘ └┘ └─┘ └───┘
typ      └┘ └┘ └─┘ └───┘
264  
265  /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
266  Let `f` and `B` be continuous functions on `[a, b]` such that
267  
268  * `∥f a∥ ≤ B a`;
269  * `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
270  * the norm of `f'` is strictly less than `B'` whenever `∥f x∥ = B x`.
271  
272  Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
273  to make this theorem work for piecewise differentiable functions.
274  -/
275  lemma image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {f' : ℝ → E}
id                                                                       
src                                                                   
typ                                                                      
276    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
277    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
278    {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                            └───────────┘    └─┘
279    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
280    (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → ∥f' x∥ < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
281    ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
282  image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary hf
id   └────────────────────────────────────────────────────────┘ └┘
src  └────────────────────────────────────────────────────────┘
typ  └────────────────────────────────────────────────────────┘ └┘
doc  └────────────────────────────────────────────────────────┘
283    (λ x hx r hr, (hf' x hx).liminf_right_slope_norm_le hr) ha hB hB' bound
id         └┘  └┘   └─┘  └┘ └────────────────────────┘  └┘  └┘ └┘ └─┘ └───┘
src                            └────────────────────────┘
typ        └┘  └┘   └─┘  └┘ └────────────────────────┘  └┘  └┘ └┘ └─┘ └───┘
doc                            └────────────────────────┘
284  
285  /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
286  Let `f` and `B` be continuous functions on `[a, b]` such that
287  
288  * `∥f a∥ ≤ B a`;
289  * `f` has right derivative `f'` at every point of `[a, b)`;
290  * `B` has derivative `B'` everywhere on `ℝ`;
291  * the norm of `f'` is strictly less than `B'` whenever `∥f x∥ = B x`.
292  
293  Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
294  to make this theorem work for piecewise differentiable functions.
295  -/
296  lemma image_norm_le_of_norm_deriv_right_lt_deriv_boundary {f' : ℝ → E}
id                                                                      
src                                                                  
typ                                                                     
297    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
298    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
299    {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id                                        └──────────┘   └┘   
src                                            └──────────┘
typ                                       └──────────┘   └┘   
doc                                                 └──────────┘
300    (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → ∥f' x∥ < B' x) :
id                   └─┘           └┘   └┘ 
src                   └─┘                      
typ                  └─┘           └┘   └┘ 
doc                   └─┘
301    ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
302  image_norm_le_of_norm_deriv_right_lt_deriv_boundary' hf hf' ha
id   └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
src  └──────────────────────────────────────────────────┘
typ  └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
doc  └──────────────────────────────────────────────────┘
303    (λ x hx, (hB x).continuous_at.continuous_within_at)
id         └┘   └┘  └───────────┘ └──────────────────┘
src                   └───────────┘ └──────────────────┘
typ        └┘   └┘  └───────────┘ └──────────────────┘
304    (λ x hx, (hB x).has_deriv_within_at) bound
id         └┘   └┘  └─────────────────┘   └───┘
src                   └─────────────────┘
typ        └┘   └┘  └─────────────────┘   └───┘
305  
306  /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
307  Let `f` and `B` be continuous functions on `[a, b]` such that
308  
309  * `∥f a∥ ≤ B a`;
310  * `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
311  * we have `∥f' x∥ ≤ B x` everywhere on `[a, b)`.
312  
313  Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
314  to make this theorem work for piecewise differentiable functions.
315  -/
316  lemma image_norm_le_of_norm_deriv_right_le_deriv_boundary' {f' : ℝ → E}
id                                                                       
src                                                                   
typ                                                                      
317    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
318    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
319    {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id                                    └───────────┘   └─┘  
src                                       └───────────┘    └─┘
typ                                   └───────────┘   └─┘  
doc                                            └───────────┘    └─┘
320    (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
321    (bound : ∀ x ∈ Ico a b, ∥f' x∥ ≤ B' x) :
id                   └─┘    └┘   └┘ 
src                   └─┘           
typ                  └─┘    └┘   └┘ 
doc                   └─┘
322    ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
323  image_le_of_liminf_slope_right_le_deriv_boundary (continuous_norm.comp_continuous_on hf) ha hB hB' $
id   └──────────────────────────────────────────────┘  └─────────────┘└─────────────────┘ └┘  └┘ └┘ └─┘
src  └──────────────────────────────────────────────┘  └─────────────┘└─────────────────┘
typ  └──────────────────────────────────────────────┘  └─────────────┘└─────────────────┘ └┘  └┘ └┘ └─┘
doc  └──────────────────────────────────────────────┘
324    (λ x hx r hr, (hf' x hx).liminf_right_slope_norm_le (lt_of_le_of_lt (bound x hx) hr))
id         └┘  └┘   └─┘  └┘ └────────────────────────┘   └────────────┘  └───┘  └┘  └┘
src                            └────────────────────────┘   └────────────┘
typ        └┘  └┘   └─┘  └┘ └────────────────────────┘   └────────────┘  └───┘  └┘  └┘
doc                            └────────────────────────┘
325  
326  /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
327  Let `f` and `B` be continuous functions on `[a, b]` such that
328  
329  * `∥f a∥ ≤ B a`;
330  * `f` has right derivative `f'` at every point of `[a, b)`;
331  * `B` has derivative `B'` everywhere on `ℝ`;
332  * we have `∥f' x∥ ≤ B x` everywhere on `[a, b)`.
333  
334  Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
335  to make this theorem work for piecewise differentiable functions.
336  -/
337  lemma image_norm_le_of_norm_deriv_right_le_deriv_boundary {f' : ℝ → E}
id                                                                      
src                                                                  
typ                                                                     
338    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
339    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
340    {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id                                        └──────────┘   └┘   
src                                            └──────────┘
typ                                       └──────────┘   └┘   
doc                                                 └──────────┘
341    (bound : ∀ x ∈ Ico a b, ∥f' x∥ ≤ B' x) :
id                   └─┘    └┘   └┘ 
src                   └─┘           
typ                  └─┘    └┘   └┘ 
doc                   └─┘
342    ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id             └─┘         
src              └─┘           
typ            └─┘         
doc               └─┘
343  image_norm_le_of_norm_deriv_right_le_deriv_boundary' hf hf' ha
id   └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
src  └──────────────────────────────────────────────────┘
typ  └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
doc  └──────────────────────────────────────────────────┘
344    (λ x hx, (hB x).continuous_at.continuous_within_at)
id         └┘   └┘  └───────────┘ └──────────────────┘
src                   └───────────┘ └──────────────────┘
typ        └┘   └┘  └───────────┘ └──────────────────┘
345    (λ x hx, (hB x).has_deriv_within_at) bound
id         └┘   └┘  └─────────────────┘   └───┘
src                   └─────────────────┘
typ        └┘   └┘  └─────────────────┘   └───┘
346  
347  /-- A function on `[a, b]` with the norm of the right derivative bounded by `C`
348  satisfies `∥f x - f a∥ ≤ C * (x - a)`. -/
349  theorem norm_image_sub_le_of_norm_deriv_right_le_segment {f' : ℝ → E} {C : ℝ}
id                                                                            
src                                                                            
typ                                                                           
350    (hf : continuous_on f (Icc a b))
id           └───────────┘   └─┘  
src          └───────────┘    └─┘
typ          └───────────┘   └─┘  
doc          └───────────┘    └─┘
351    (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id                 └─┘    └─────────────────┘   └┘    └─┘   
src                 └─┘      └─────────────────┘           └─┘
typ                └─┘    └─────────────────┘   └┘    └─┘   
doc                 └─┘      └─────────────────┘           └─┘
352    (bound : ∀x ∈ Ico a b, ∥f' x∥ ≤ C) :
id                  └─┘    └┘   
src                  └─┘           
typ                 └─┘    └┘   
doc                  └─┘
353    ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id          └─┘               
src          └─┘                      
typ         └─┘               
doc          └─┘
354  begin
st   └─────
355    let g := λ x, f x - f a,
id                         
src    └───────┘ └──┘   
typ    └───────┘ └──┘  
doc    └───────┘ └──┘    
txt    └───────┘ └──┘    
par    └───────┘ └──┘    
pid    └───┘└─┘ └──┘    
st   ────────────────────────┘└─
356    have hg : continuous_on g (Icc a b), from hf.sub continuous_on_const,
id               └───────────┘   └─┘          └────┘ └─────────────────┘
src    └────────┘└───────────┘  └─┘    └───┘└────┘└─────────────────┘
typ    └────────┘└───────────┘ └─┘  └───┘└────┘└─────────────────┘
doc    └────────┘└───────────┘  └─┘    └───┘      
txt    └────────┘                      └───┘      
par    └────────┘                      └───┘      
pid    └─────┘└─┘                      └───┘      
st   ────────────────────────────────────┘└───────────────────────────────┘└─
357    have hg' : ∀ x ∈ Ico a b, has_deriv_within_at g (f' x) (Ioi x) x,
id                      └─┘    └─────────────────┘   └┘     └─┘
src    └─────────┘ └───┘└─┘   └─────────────────┘     └┘ └─┘ └┘
typ    └─────────┘ └───┘└─┘ └─────────────────┘ └┘ └┘ └─┘ └┘
doc    └─────────┘ └───┘└─┘   └─────────────────┘     └┘ └─┘ └┘
txt    └─────────┘ └───┘                              └┘     └┘
par    └─────────┘ └───┘                              └┘     └┘
pid    └──────┘└─┘ └───┘                              └┘     └┘
st   ─────────────────────────────────────────────────────────────────┘└─
358    { assume x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
359      simpa using (hf' x hx).sub (has_deriv_within_at_const _ _ _) },
id                    └─┘  └┘       └───────────────────────┘
src      └──────────┘       └────┘ └───────────────────────┘└──────┘
typ      └──────────┘ └─┘└┘└────┘ └───────────────────────┘└──────┘
doc      └──────────┘       └────┘                          └──────┘
txt      └──────────┘       └────┘                          └──────┘
par      └──────────┘       └────┘                          └──────┘
pid           └────┘       └────┘                          └─────┘
st   ────────────────────────────────────────────────────────────────┘└┘
360    let B := λ x, C * (x - a),
id                          
src    └───────┘ └──┘     
typ    └───────┘ └──┘   
doc    └───────┘ └──┘      
txt    └───────┘ └──┘      
par    └───────┘ └──┘      
pid    └───┘└─┘ └──┘      
st   ──────────────────────────┘└─
361    have hB : ∀ x, has_deriv_at B C x,
id                    └──────────┘  
src    └────────┘ └┘ └──────────┘  
typ    └────────┘ └┘ └──────────┘
doc    └────────┘ └┘ └──────────┘  
txt    └────────┘ └┘               
par    └────────┘ └┘               
pid    └─────┘└─┘ └┘               
st   ──────────────────────────────────┘└─
362    { assume x,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
363      simpa using (has_deriv_at_const x C).mul ((has_deriv_at_id x).sub (has_deriv_at_const x a)) },
id                                                 └─────────────┘         └────────────────┘  
src      └──────────┘                     └────┘  └─────────────┘ └────┘ └────────────────┘  └─┘
typ      └──────────┘                    └────┘  └─────────────┘ └────┘ └────────────────┘└─┘
doc      └──────────┘                     └────┘                  └────┘                     └─┘
txt      └──────────┘                     └────┘                  └────┘                     └─┘
par      └──────────┘                     └────┘                  └────┘                     └─┘
pid           └────┘                     └────┘                  └────┘                     └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└┘
364    convert image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound,
id             └─────────────────────────────────────────────────┘ └┘ └─┘   └┘ └───┘
src    └──────┘└─────────────────────────────────────────────────┘     └─┘  
typ    └──────┘└─────────────────────────────────────────────────┘└┘└─┘└─┘└┘└───┘
doc    └──────┘└─────────────────────────────────────────────────┘     └─┘  
txt    └──────┘                                                        └─┘  
par    └──────┘                                                        └─┘  
pid                                                                   └─┘  
st   ──────────────────────────────────────────────────────────────────────────────┘└─
365    { simp only [g, B] },
id                    
src      └─────────┘ └┘ └┘
typ      └─────────┘└┘└┘
doc      └─────────┘ └┘ └┘
txt      └─────────┘ └┘ └┘
par      └─────────┘ └┘ └┘
pid          └──┘└┘ └┘ 
st   ───┘└───────────────┘└┘
366    { simp only [g, B], rw [sub_self, _root_.norm_zero, sub_self, mul_zero] }
id                           └──────┘  └──────────────┘  └──────┘  └──────┘
src      └─────────┘ └┘   └──┘└──────┘└┘└──────────────┘└┘└──────┘└┘└──────┘└┘
typ      └─────────┘└┘  └──┘└──────┘└┘└──────────────┘└┘└──────┘└┘└──────┘└┘
doc      └─────────┘ └┘   └──┘        └┘                └┘        └┘        └┘
txt      └─────────┘ └┘   └──┘        └┘                └┘        └┘        └┘
par      └─────────┘ └┘   └──┘        └┘                └┘        └┘        └┘
pid          └──┘└┘ └┘     └┘        └┘                └┘        └┘        
st   ───────────────────┘└────────────┘└────────────────┘└────────┘└────────┘└─
367  end
st   ──┘
368  
369  /-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
370  bounded by `C` satisfies `∥f x - f a∥ ≤ C * (x - a)`, `has_deriv_within_at`
371  version. -/
372  theorem norm_image_sub_le_of_norm_deriv_le_segment' {f' : ℝ → E} {C : ℝ}
id                                                                       
src                                                                       
typ                                                                      
373    (hf : ∀ x ∈ Icc a b, has_deriv_within_at f (f' x) (Icc a b) x)
id                └─┘    └─────────────────┘   └┘    └─┘    
src                └─┘      └─────────────────┘           └─┘
typ               └─┘    └─────────────────┘   └┘    └─┘    
doc                └─┘      └─────────────────┘           └─┘
374    (bound : ∀x ∈ Ico a b, ∥f' x∥ ≤ C) :
id                  └─┘    └┘   
src                  └─┘           
typ                 └─┘    └┘   
doc                  └─┘
375    ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id          └─┘               
src          └─┘                      
typ         └─┘               
doc          └─┘
376  begin
st   └─────
377    refine norm_image_sub_le_of_norm_deriv_right_le_segment
id            └──────────────────────────────────────────────┘
src    └─────┘└──────────────────────────────────────────────┘
typ    └─────┘└──────────────────────────────────────────────┘
doc    └─────┘└──────────────────────────────────────────────┘
txt    └─────┘                                                
par    └─────┘                                                
pid                                                          
st   ──────────────────────────────────────────────────────────
378      (λ x hx, (hf x hx).continuous_within_at) (λ x hx, _) bound,
id                 └┘                                         └───┘
src  ───┘  └─────┘      └──────────────────────┘  └────────┘
typ  ───┘  └─────┘ └┘   └──────────────────────┘  └────────┘└───┘
doc  ───┘  └─────┘      └──────────────────────┘  └────────┘
txt  ───┘  └─────┘      └──────────────────────┘  └────────┘
par  ───┘  └─────┘      └──────────────────────┘  └────────┘
pid  ───┘  └─────┘      └──────────────────────┘  └────────┘
st   ─────────────────────────────────────────────────────────────┘└─
379    apply (hf x $ Ico_subset_Icc_self hx).nhds_within,
id            └┘    └─────────────────┘ └┘
src    └────┘     └─────────────────┘  └───────────┘
typ    └────┘ └┘ └─────────────────┘└┘└───────────┘
doc    └────┘                          └───────────┘
txt    └────┘                          └───────────┘
par    └────┘                          └───────────┘
pid                                   └──────────┘
st   ──────────────────────────────────────────────────┘└─
380    exact Icc_mem_nhds_within_Ioi hx
id           └─────────────────────┘ └┘
src    └────┘└─────────────────────┘  
typ    └────┘└─────────────────────┘└┘
doc    └────┘                         
txt    └────┘                         
par    └────┘                         
pid                                  
st   ──────────────────────────────────┘
381  end
st   └─┘
382  
383  /-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
384  bounded by `C` satisfies `∥f x - f a∥ ≤ C * (x - a)`, `deriv_within`
385  version. -/
386  theorem norm_image_sub_le_of_norm_deriv_le_segment {C : ℝ} (hf : differentiable_on ℝ f (Icc a b))
id                                                                   └───────────────┘    └─┘  
src                                                                  └───────────────┘     └─┘
typ                                                                  └───────────────┘    └─┘  
doc                                                                   └───────────────┘      └─┘
387    (bound : ∀x ∈ Ico a b, ∥deriv_within f (Icc a b) x∥ ≤ C) :
id                  └─┘    └──────────┘   └─┘      
src                  └─┘      └──────────┘    └─┘        
typ                 └─┘    └──────────┘   └─┘      
doc                  └─┘       └──────────┘    └─┘
388    ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id          └─┘               
src          └─┘                      
typ         └─┘               
doc          └─┘
389  begin
st   └─────
390    refine norm_image_sub_le_of_norm_deriv_le_segment' _ bound,
id            └─────────────────────────────────────────┘   └───┘
src    └─────┘└─────────────────────────────────────────┘└─┘
typ    └─────┘└─────────────────────────────────────────┘└─┘└───┘
doc    └─────┘└─────────────────────────────────────────┘└─┘
txt    └─────┘                                           └─┘
par    └─────┘                                           └─┘
pid                                                     └─┘
st   ───────────────────────────────────────────────────────────┘└─
391    exact λ x hx, (hf x  hx).has_deriv_within_at
id                    └┘
src    └────┘ └─────┘    └┘  └────────────────────┘
typ    └────┘ └─────┘ └┘ └┘  └────────────────────┘
doc    └────┘ └─────┘    └┘  └────────────────────┘
txt    └────┘ └─────┘    └┘  └────────────────────┘
par    └────┘ └─────┘    └┘  └────────────────────┘
pid          └─────┘    └┘  └──────────────────┘└┘
st   ──────────────────────────────────────────────┘
392  end
st   └─┘
393  
394  /-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
395  bounded by `C` satisfies `∥f 1 - f 0∥ ≤ C`, `has_deriv_within_at`
396  version. -/
397  theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {f' : ℝ → E} {C : ℝ}
id                                                                          
src                                                                          
typ                                                                         
398    (hf : ∀ x ∈ Icc (0:ℝ) 1, has_deriv_within_at f (f' x) (Icc (0:ℝ) 1) x)
id                └─┘         └─────────────────┘   └┘    └─┘         
src                └─┘         └─────────────────┘           └─┘    
typ               └─┘         └─────────────────┘   └┘    └─┘         
doc                └─┘          └─────────────────┘           └─┘
399    (bound : ∀x ∈ Ico (0:ℝ) 1, ∥f' x∥ ≤ C) :
id                  └─┘         └┘   
src                  └─┘              
typ                 └─┘         └┘   
doc                  └─┘
400    ∥f 1 - f 0∥ ≤ C :=
id             
src             
typ            
401  by simpa only [sub_zero, mul_one]
id                  └──────┘  └─────┘
src     └──────────┘└──────┘└┘└─────┘└─
typ     └──────────┘└──────┘└┘└─────┘└─
doc     └──────────┘        └┘       └─
txt     └──────────┘        └┘       └─
par     └──────────┘        └┘       └─
pid          └──┘└┘        └┘       
st     └───────────────────────────────
402    using norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)
id           └─────────────────────────────────────────┘ └┘ └───┘    └───────────┘   └─────────┘
src  ───────┘└─────────────────────────────────────────┘       └─┘ └───────────┘└─┘└─────────┘└─
typ  ───────┘└─────────────────────────────────────────┘└┘└───┘└─┘ └───────────┘└─┘└─────────┘└─
doc  ───────┘└─────────────────────────────────────────┘       └─┘              └─┘           └─
txt  ───────┘                                                  └─┘              └─┘           └─
par  ───────┘                                                  └─┘              └─┘           └─
pid  ─┘└────┘                                                  └─┘              └─┘           
st   ─────────────────────────────────────────────────────────────────────────────────────────────
403  
src  
typ  
doc  
txt  
par  
pid  
st   
404  /-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
405  bounded by `C` satisfies `∥f 1 - f 0∥ ≤ C`, `deriv_within` version. -/
406  theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {C : ℝ}
id                                                              
src                                                             
typ                                                             
407    (hf : differentiable_on ℝ f (Icc (0:ℝ) 1))
id           └───────────────┘    └─┘    
src          └───────────────┘     └─┘    
typ          └───────────────┘    └─┘    
doc          └───────────────┘      └─┘
408    (bound : ∀x ∈ Ico (0:ℝ) 1, ∥deriv_within f (Icc (0:ℝ) 1) x∥ ≤ C) :
id                  └─┘         └──────────┘   └─┘           
src                  └─┘         └──────────┘    └─┘           
typ                 └─┘         └──────────┘   └─┘           
doc                  └─┘           └──────────┘    └─┘
409    ∥f 1 - f 0∥ ≤ C :=
id             
src             
typ            
410  by simpa only [sub_zero, mul_one]
id                  └──────┘  └─────┘
src     └──────────┘└──────┘└┘└─────┘└─
typ     └──────────┘└──────┘└┘└─────┘└─
doc     └──────────┘        └┘       └─
txt     └──────────┘        └┘       └─
par     └──────────┘        └┘       └─
pid          └──┘└┘        └┘       
st     └───────────────────────────────
411    using norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)
id           └────────────────────────────────────────┘ └┘ └───┘    └───────────┘   └─────────┘
src  ───────┘└────────────────────────────────────────┘       └─┘ └───────────┘└─┘└─────────┘└─
typ  ───────┘└────────────────────────────────────────┘└┘└───┘└─┘ └───────────┘└─┘└─────────┘└─
doc  ───────┘└────────────────────────────────────────┘       └─┘              └─┘           └─
txt  ───────┘                                                 └─┘              └─┘           └─
par  ───────┘                                                 └─┘              └─┘           └─
pid  ─┘└────┘                                                 └─┘              └─┘           
st   ────────────────────────────────────────────────────────────────────────────────────────────
412  
src  
typ  
doc  
txt  
par  
pid  
st   
413  end
414  
415  /-! ### Vector-valued functions `f : E → F` -/
416  
417  /-- The mean value theorem on a convex set: if the derivative of a function is bounded by C, then
418  the function is C-Lipschitz -/
419  theorem convex.norm_image_sub_le_of_norm_deriv_le {f : E → F} {C : ℝ} {s : set E} {x y : E}
id                                                                           └─┘          
src                                                                            └─┘
typ                                                                          └─┘          
420    (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥fderiv_within ℝ f s x∥ ≤ C)
id           └───────────────┘                  └───────────┘      
src          └───────────────┘                      └───────────┘        
typ          └───────────────┘                  └───────────┘      
doc          └───────────────┘                        └───────────┘
421    (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
id           └────┘                                   
src          └────┘                                               
typ          └────┘                                   
doc          └────┘
422  begin
st   └─────
423    /- By composition with t ↦ x + t • (y-x), we reduce to a statement for functions defined
st   ───────────────────────────────────────────────────────────────────────────────────────────
424    on [0,1], for which it is proved in `norm_image_sub_le_of_norm_deriv_le_segment`.
st   ────────────────────────────────────────────────────────────────────────────────────
425    We just have to check the differentiability of the composition and bounds on its derivative,
st   ───────────────────────────────────────────────────────────────────────────────────────────────
426    which is straightforward but tedious for lack of automation. -/
st   ──────────────────────────────────────────────────────────────────
427    have C0 : 0 ≤ C := le_trans (norm_nonneg _) (bound x xs),
id                      └──────┘  └─────────┘     └───┘  └┘
src    └──────────┘ └──┘└──────┘ └─────────┘└──┘         
typ    └──────────┘└──┘└──────┘ └─────────┘└──┘ └───┘└┘
doc    └──────────┘  └──┘                    └──┘         
txt    └──────────┘  └──┘                    └──┘         
par    └──────────┘  └──┘                    └──┘         
pid    └─────┘└───┘  └──┘                    └──┘         
st   ─────────────────────────────────────────────────────────┘└─
428    set g : ℝ → E := λ t, x + t • (y - x),
id                                   
src    └──────┘   └──┘ └──┘     
typ    └──────┘  └──┘ └──┘   
doc    └──────┘   └──┘ └──┘        
txt    └──────┘   └──┘ └──┘        
par    └──────┘   └──┘ └──┘        
pid       └─┘   └─┘ └──┘        
st   ──────────────────────────────────────┘└─
429    have Dg : ∀ t, has_deriv_at g (y-x) t,
id                    └──────────┘    
src    └────────┘ └┘ └──────────┘     └┘
typ    └────────┘ └┘ └──────────┘  └┘
doc    └────────┘ └┘ └──────────┘     └┘
txt    └────────┘ └┘                  └┘
par    └────────┘ └┘                  └┘
pid    └─────┘└─┘ └┘                  └┘
st   ──────────────────────────────────────┘└─
430    { assume t,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
431      simpa only [one_smul] using ((has_deriv_at_id t).smul_const (y - x)).const_add x },
id                   └──────┘          └─────────────┘                                
src      └──────────┘└──────┘└──────┘  └─────────────┘ └───────────┘    └───────────┘ 
typ      └──────────┘└──────┘└──────┘  └─────────────┘└───────────┘   └───────────┘
doc      └──────────┘        └──────┘                  └───────────┘    └───────────┘ 
txt      └──────────┘        └──────┘                  └───────────┘    └───────────┘ 
par      └──────────┘        └──────┘                  └───────────┘    └───────────┘ 
pid           └──┘└┘        └────┘                  └───────────┘    └───────────┘ 
st   ────────────────────────────────────────────────────────────────────────────────────┘└┘
432    have segm : Icc 0 1 ⊆ g ⁻¹' s,
id                 └─┘       └─┘ 
src    └──────────┘└─┘└───┘ └─┘
typ    └──────────┘└─┘└───┘└─┘
doc    └──────────┘└─┘└───┘  └─┘
txt    └──────────┘   └───┘     
par    └──────────┘   └───┘     
pid    └───────┘└─┘   └───┘     
st   ──────────────────────────────┘└─
433    { rw [← image_subset_iff, ← segment_eq_image'],
id             └──────────────┘    └───────────────┘
src      └────┘└──────────────┘└──┘└───────────────┘
typ      └────┘└──────────────┘└──┘└───────────────┘
doc      └────┘└──────────────┘└──┘                 
txt      └────┘                └──┘                 
par      └────┘                └──┘                 
pid        └──┘                └──┘                 
st   ───┘└────────────────────┘└───────────────────┘└──
434      apply hs.segment_subset xs ys },
id             └───────────────┘ └┘ └┘
src      └────┘└───────────────┘    
typ      └────┘└───────────────┘└┘└┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ─────────────────────────────────┘└┘
435    have : f x = f (g 0), by { simp only [g], rw [zero_smul, add_zero] },
id                                              └───────┘  └──────┘
src    └─────┘     └─┘       └─────────┘   └──┘└───────┘└┘└──────┘└┘
typ    └─────┘  └─┘       └─────────┘  └──┘└───────┘└┘└──────┘└┘
doc    └─────┘      └─┘       └─────────┘   └──┘         └┘        └┘
txt    └─────┘      └─┘       └─────────┘   └──┘         └┘        └┘
par    └─────┘      └─┘       └─────────┘   └──┘         └┘        └┘
pid    └───┘└┘      └─┘           └──┘└┘     └┘         └┘        
st   ─────────────────────┘     └────────────┘└─────────────┘└────────┘└┘
436    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
437    have : f y = f (g 1), by { simp only [g], rw [one_smul, add_sub_cancel'_right] },
id                                               └──────┘  └───────────────────┘
src    └─────┘      └─┘       └─────────┘   └──┘└──────┘└┘└───────────────────┘└┘
typ    └─────┘   └─┘       └─────────┘  └──┘└──────┘└┘└───────────────────┘└┘
doc    └─────┘      └─┘       └─────────┘   └──┘        └┘                     └┘
txt    └─────┘      └─┘       └─────────┘   └──┘        └┘                     └┘
par    └─────┘      └─┘       └─────────┘   └──┘        └┘                     └┘
pid    └───┘└┘      └─┘           └──┘└┘     └┘        └┘                     
st   ─────────────────────┘     └────────────┘└────────────┘└─────────────────────┘└┘
438    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
439    have D2: ∀ t ∈ Icc (0:ℝ) 1, has_deriv_within_at (f ∘ g)
id                                 └─────────────────┘    
src    └───────┘ └───┘    └┘ └─┘ └─────────────────┘   └─
typ    └───────┘ └───┘    └┘ └─┘ └─────────────────┘   └─
doc    └───────┘ └───┘    └┘ └─┘ └─────────────────┘    └─
txt    └───────┘ └───┘    └┘ └─┘                        └─
par    └───────┘ └───┘    └┘ └─┘                        └─
pid    └─────┘└┘ └───┘    └┘ └─┘                        └─
st   ──────────────────────────────────────────────────────────
440      ((fderiv_within ℝ f s (g t) : E → F) (y-x)) (Icc (0:ℝ) 1) t,
id         └───────────┘                       └─┘
src  ───┘  └───────────┘      └──┘   └┘    └─┘ └─┘ └┘ └───┘
typ  ───┘  └───────────┘   └──┘ └┘  └─┘ └─┘ └┘ └───┘
doc  ───┘  └───────────┘      └──┘   └┘    └─┘ └─┘ └┘ └───┘
txt  ───┘                     └──┘   └┘    └─┘     └┘ └───┘
par  ───┘                     └──┘   └┘    └─┘     └┘ └───┘
pid  ───┘                     └──┘   └┘    └─┘     └┘ └───┘
st   ──────────────────────────────────────────────────────────────┘└─
441    { intros t ht,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
442      exact (hf (g t) $ segm ht).has_fderiv_within_at.comp_has_deriv_within_at _
id              └┘             └┘
src      └────┘      └┘       └─────────────────────────────────────────────────
typ      └────┘ └┘  └┘     └┘└─────────────────────────────────────────────────
doc      └────┘      └┘       └─────────────────────────────────────────────────
txt      └────┘      └┘       └─────────────────────────────────────────────────
par      └────┘      └┘       └─────────────────────────────────────────────────
pid                 └┘       └─────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────
443        (Dg t).has_deriv_within_at segm },
id          └┘                       └──┘
src  ─────┘    └────────────────────┘    
typ  ─────┘ └┘└────────────────────┘└──┘
doc  ─────┘    └────────────────────┘    
txt  ─────┘    └────────────────────┘    
par  ─────┘    └────────────────────┘    
pid  ─────┘    └────────────────────┘    
st   ─────────────────────────────────────┘└┘
444    apply norm_image_sub_le_of_norm_deriv_le_segment_01' D2,
id           └────────────────────────────────────────────┘ └┘
src    └────┘└────────────────────────────────────────────┘
typ    └────┘└────────────────────────────────────────────┘└┘
doc    └────┘└────────────────────────────────────────────┘
txt    └────┘                                              
par    └────┘                                              
pid                                                       
st   ────────────────────────────────────────────────────────┘└─
445    assume t ht,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
446    refine le_trans (le_op_norm _ _) (mul_le_mul_of_nonneg_right _ (norm_nonneg _)),
id            └──────┘  └────────┘       └────────────────────────┘    └─────────┘
src    └─────┘└──────┘ └────────┘└────┘ └────────────────────────┘└─┘ └─────────┘└──┘
typ    └─────┘└──────┘ └────────┘└────┘ └────────────────────────┘└─┘ └─────────┘└──┘
doc    └─────┘         └────────┘└────┘                           └─┘            └──┘
txt    └─────┘                   └────┘                           └─┘            └──┘
par    └─────┘                   └────┘                           └─┘            └──┘
pid                             └────┘                           └─┘            └──┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
447    exact bound (g t) (segm $ Ico_subset_Icc_self ht)
id           └───┘      └──┘   └─────────────────┘ └┘
src    └────┘        └┘      └─────────────────┘  └┘
typ    └────┘└───┘ └┘ └──┘ └─────────────────┘└┘└┘
doc    └────┘        └┘                           └┘
txt    └────┘        └┘                           └┘
par    └────┘        └┘                           └┘
pid                 └┘                           
st   ───────────────────────────────────────────────────┘
448  end
st   └─┘
449  
450  /-- If a function has zero Fréchet derivative at every point of a convex set,
451  then it is a constant on this set. -/
452  theorem convex.is_const_of_fderiv_within_eq_zero {s : set E} (hs : convex s)
id                                                         └─┘         └────┘ 
src                                                        └─┘          └────┘
typ                                                        └─┘         └────┘ 
doc                                                                     └────┘
453    {f : E → F} (hf : differentiable_on ℝ f s) (hf' : ∀ x ∈ s, fderiv_within ℝ f s x = 0)
id                     └───────────────┘                   └───────────┘     
src                      └───────────────┘                       └───────────┘        
typ                    └───────────────┘                   └───────────┘     
doc                      └───────────────┘                        └───────────┘
454    {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
id                                
src                                  
typ                               
455    f x = f y :=
id         
src        
typ        
456  have bound : ∀ x ∈ s, ∥fderiv_within ℝ f s x∥ ≤ 0,
id                       └───────────┘     
src                        └───────────┘        
typ                      └───────────┘     
doc                         └───────────┘
457    from λ x hx, by simp only [hf' x hx, _root_.norm_zero],
id             └┘                └─┘  └┘  └──────────────┘
src                    └─────────┘      └┘└──────────────┘
typ            └┘     └─────────┘└─┘└┘└┘└──────────────┘
doc                    └─────────┘      └┘                
txt                    └─────────┘      └┘                
par                    └─────────┘      └┘                
pid                        └──┘└┘      └┘                
st                    └─────────────────────────────────────┘
458  by simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm]
id                   └──────────┘            └──────┘  └──────────┘  └─────┘
src     └──────────┘ └──────────┘└──────────┘└──────┘└┘└──────────┘└┘└─────┘└─
typ     └──────────┘ └──────────┘└──────────┘└──────┘└┘└──────────┘└┘└─────┘└─
doc     └──────────┘             └──────────┘        └┘            └┘       └─
txt     └──────────┘             └──────────┘        └┘            └┘       └─
par     └──────────┘             └──────────┘        └┘            └┘       └─
pid          └──┘└┘             └──────────┘        └┘            └┘       
st     └──────────────────────────────────────────────────────────────────────
459    using hs.norm_image_sub_le_of_norm_deriv_le hf bound hx hy
id           └───────────────────────────────────┘ └┘ └───┘ └┘ └┘
src  ───────┘└───────────────────────────────────┘           
typ  ───────┘└───────────────────────────────────┘└┘└───┘└┘└┘
doc  ───────┘└───────────────────────────────────┘           
txt  ───────┘                                                
par  ───────┘                                                
pid  ─┘└────┘                                                
st   ─────────────────────────────────────────────────────────────
460  
src  
typ  
doc  
txt  
par  
pid  
st   
461  theorem is_const_of_fderiv_eq_zero {f : E → F} (hf : differentiable ℝ f)
id                                                      └────────────┘  
src                                                       └────────────┘ 
typ                                                     └────────────┘  
doc                                                       └────────────┘
462    (hf' : ∀ x, fderiv ℝ f x = 0) (x y : E) :
id                └────┘               
src                └────┘      
typ               └────┘               
doc                └────┘
463    f x = f y :=
id         
src        
typ        
464  convex_univ.is_const_of_fderiv_within_eq_zero hf.differentiable_on
id   └─────────┘└────────────────────────────────┘ └┘└────────────────┘
src  └─────────┘└────────────────────────────────┘   └────────────────┘
typ  └─────────┘└────────────────────────────────┘ └┘└────────────────┘
doc             └────────────────────────────────┘
465    (λ x _, by rw fderiv_within_univ; exact hf' x) trivial trivial
id                 └────────────────┘        └─┘   └─────┘ └─────┘
src               └─┘└────────────────┘  └────┘      └─────┘ └─────┘
typ             └─┘└────────────────┘  └────┘└─┘  └─────┘ └─────┘
doc               └─┘                    └────┘   
txt               └─┘                    └────┘   
par               └─┘                    └────┘   
pid                                             
st               └─────────────────────────────────┘
466  
467  /-! ### Functions `[a, b] → ℝ`. -/
468  
469  section interval
470  
471  -- Declare all variables here to make sure they come in a correct order
472  variables (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (Icc a b))
id                                                      └───────────┘    └─┘
src                                                      └───────────┘    └─┘
typ                                                     └───────────┘    └─┘
doc                                                          └───────────┘    └─┘
473    (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) (hfd : differentiable_on ℝ f (Ioo a b))
id                  └─┘      └──────────┘                  └───────────────┘     └─┘
src                  └─┘      └──────────┘                    └───────────────┘     └─┘
typ                 └─┘      └──────────┘                  └───────────────┘     └─┘
doc                  └─┘      └──────────┘                    └───────────────┘      └─┘
474    (g g' : ℝ → ℝ) (hgc : continuous_on g (Icc a b)) (hgg' : ∀ x ∈ Ioo a b, has_deriv_at g (g' x) x)
id                         └───────────┘    └─┘                    └─┘      └──────────┘         
src                        └───────────┘    └─┘                     └─┘      └──────────┘
typ                        └───────────┘    └─┘                    └─┘      └──────────┘         
doc                          └───────────┘    └─┘                     └─┘      └──────────┘
475    (hgd : differentiable_on ℝ g (Ioo a b))
id            └───────────────┘     └─┘
src           └───────────────┘     └─┘
typ           └───────────────┘     └─┘
doc           └───────────────┘      └─┘
476  
477  include hab hfc hff' hgc hgg'
478  
479  /-- Cauchy's Mean Value Theorem, `has_deriv_at` version. -/
480  lemma exists_ratio_has_deriv_at_eq_ratio_slope :
481    ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c :=
id         └─┘           └┘           └┘ 
src         └─┘                                  
typ        └─┘           └┘           └┘ 
doc          └─┘
482  begin
st   └─────
483    let h := λ x, (g b - g a) * f x - (f b - f a) * g x,
id                                                
src    └───────┘ └──┘     └┘         └┘  
typ    └───────┘ └──┘     └┘      └┘ 
doc    └───────┘ └──┘      └┘          └┘  
txt    └───────┘ └──┘      └┘          └┘  
par    └───────┘ └──┘      └┘          └┘  
pid    └───┘└─┘ └──┘      └┘          └┘  
st   ────────────────────────────────────────────────────┘└─
484    have hI : h a = h b,
id                    
src    └────────┘   
typ    └────────┘ 
doc    └────────┘    
txt    └────────┘    
par    └────────┘    
pid    └─────┘└─┘    
st   ────────────────────┘└─
485    { simp only [h], ring },
id                  
src      └─────────┘   └───┘
typ      └─────────┘  └───┘
doc      └─────────┘   └───┘
txt      └─────────┘   └───┘
par      └─────────┘   └───┘
pid          └──┘└┘       
st   ───┘└───────────┘└─────┘└┘
486    let h' := λ x, (g b - g a) * f' x - (f b - f a) * g' x,
id                                 └┘                └┘
src    └────────┘ └──┘      └┘           └┘   
typ    └────────┘ └──┘     └┘ └┘     └┘ └┘
doc    └────────┘ └──┘      └┘           └┘   
txt    └────────┘ └──┘      └┘           └┘   
par    └────────┘ └──┘      └┘           └┘   
pid    └────┘└─┘ └──┘      └┘           └┘   
st   ───────────────────────────────────────────────────────┘└─
487    have hhh' : ∀ x ∈ Ioo a b, has_deriv_at h (h' x) x,
id                       └─┘    └──────────┘   └┘
src    └──────────┘ └───┘└─┘   └──────────┘     └┘
typ    └──────────┘ └───┘└─┘ └──────────┘ └┘ └┘
doc    └──────────┘ └───┘└─┘   └──────────┘     └┘
txt    └──────────┘ └───┘                       └┘
par    └──────────┘ └───┘                       └┘
pid    └───────┘└─┘ └───┘                       └┘
st   ───────────────────────────────────────────────────┘└─
488      from λ x hx, ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a)),
id                      └──┘                                   └──┘                        
src      └───┘ └─────┘         └──────────┘      └─────┘         └──────────┘      └┘
typ      └───┘ └─────┘  └──┘   └──────────┘     └─────┘  └──┘   └──────────┘   └┘
doc      └───┘ └─────┘         └──────────┘      └─────┘         └──────────┘      └┘
txt      └───┘ └─────┘         └──────────┘      └─────┘         └──────────┘      └┘
par      └───┘ └─────┘         └──────────┘      └─────┘         └──────────┘      └┘
pid      └───┘ └─────┘         └──────────┘      └─────┘         └──────────┘      └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
489    have hhc : continuous_on h (Icc a b),
id                └───────────┘   └─┘  
src    └─────────┘└───────────┘  └─┘  
typ    └─────────┘└───────────┘ └─┘
doc    └─────────┘└───────────┘  └─┘  
txt    └─────────┘                    
par    └─────────┘                    
pid    └──────┘└─┘                    
st   ─────────────────────────────────────┘└─
490      from (continuous_on_const.mul hfc).sub (continuous_on_const.mul hgc),
id                                     └─┘       └─────────────────────┘ └─┘
src      └───┘                           └────┘ └─────────────────────┘   
typ      └───┘                        └─┘└────┘ └─────────────────────┘└─┘
doc      └───┘                           └────┘                           
txt      └───┘                           └────┘                           
par      └───┘                           └────┘                           
pid      └───┘                           └────┘                           
st   ───────────────────────────────────────────────────────────────────────┘└─
491    rcases exists_has_deriv_at_eq_zero h h' hab hhc hI hhh' with ⟨c, cmem, hc⟩,
id            └─────────────────────────┘  └┘ └─┘ └─┘ └┘ └──┘
src    └─────┘└─────────────────────────┘               └─────────────────┘
typ    └─────┘└─────────────────────────┘└┘└─┘└─┘└┘└──┘└─────────────────┘
doc    └─────┘└─────────────────────────┘               └─────────────────┘
txt    └─────┘                                          └─────────────────┘
par    └─────┘                                          └─────────────────┘
pid                                                    └─────────────────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
492    exact ⟨c, cmem, sub_eq_zero.1 hc⟩
id              └──┘  └─────────┘   └┘
src    └────┘  └┘    └┘└─────────┘└─┘  └┘
typ    └────┘ └┘└──┘└┘└─────────┘└─┘└┘└┘
doc    └────┘  └┘    └┘           └─┘  └┘
txt    └────┘  └┘    └┘           └─┘  └┘
par    └────┘  └┘    └┘           └─┘  └┘
pid           └┘    └┘           └─┘  
st   ───────────────────────────────────┘
493  end
st   └─┘
494  
495  omit hgc hgg'
496  
497  /-- Lagrange's Mean Value Theorem, `has_deriv_at` version -/
498  lemma exists_has_deriv_at_eq_slope : ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a) :=
id                                            └─┘   └┘              
src                                            └─┘                          
typ                                           └─┘   └┘              
doc                                             └─┘
499  begin
st   └─────
500    rcases exists_ratio_has_deriv_at_eq_ratio_slope f f' hab hfc hff'
id            └──────────────────────────────────────┘  └┘ └─┘ └─┘ └──┘
src    └─────┘└──────────────────────────────────────┘             
typ    └─────┘└──────────────────────────────────────┘└┘└─┘└─┘└──┘
doc    └─────┘└──────────────────────────────────────┘             
txt    └─────┘                                                     
par    └─────┘                                                     
pid                                                               
st   ────────────────────────────────────────────────────────────────────
501      id 1 continuous_id.continuous_on (λ x hx, has_deriv_at_id x) with ⟨c, cmem, hc⟩,
id       └┘   └─────────────────────────┘          └─────────────┘
src  ───┘└┘└─┘└─────────────────────────┘  └─────┘└─────────────┘ └──────────────────┘
typ  ───┘└┘└─┘└─────────────────────────┘  └─────┘└─────────────┘ └──────────────────┘
doc  ───┘  └─┘                             └─────┘                └──────────────────┘
txt  ───┘  └─┘                             └─────┘                └──────────────────┘
par  ───┘  └─┘                             └─────┘                └──────────────────┘
pid  ───┘  └─┘                             └─────┘                └──────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
502    use [c, cmem],
id            └──┘
src    └───┘ └┘    
typ    └───┘└┘└──┘
doc    └───┘ └┘    
txt    └───┘ └┘    
par    └───┘ └┘    
pid       └┘ └┘    
st   ──────────────┘└─
503    simp only [_root_.id, pi.one_apply, mul_one] at hc,
id                └───────┘  └──────────┘  └─────┘
src    └─────────┘└───────┘└┘└──────────┘└┘└─────┘└─────┘
typ    └─────────┘└───────┘└┘└──────────┘└┘└─────┘└─────┘
doc    └─────────┘         └┘            └┘       └─────┘
txt    └─────────┘         └┘            └┘       └─────┘
par    └─────────┘         └┘            └┘       └─────┘
pid        └──┘└┘         └┘            └┘       └───┘
st   ───────────────────────────────────────────────────┘└─
504    rw [← hc, mul_div_cancel_left],
id           └┘  └─────────────────┘
src    └────┘  └┘└─────────────────┘
typ    └────┘└┘└┘└─────────────────┘
doc    └────┘  └┘                   
txt    └────┘  └┘                   
par    └────┘  └┘                   
pid      └──┘  └┘                   
st   ─────────┘└───────────────────┘└──
505    exact ne_of_gt (sub_pos.2 hab)
id           └──────┘  └─────┘   └─┘
src    └────┘└──────┘ └─────┘└─┘   └┘
typ    └────┘└──────┘ └─────┘└─┘└─┘└┘
doc    └────┘                └─┘   └┘
txt    └────┘                └─┘   └┘
par    └────┘                └─┘   └┘
pid                         └─┘   
st   ────────────────────────────────┘
506  end
st   └─┘
507  
508  omit hff'
509  
510  /-- Cauchy's Mean Value Theorem, `deriv` version. -/
511  lemma exists_ratio_deriv_eq_ratio_slope :
512    ∃ c ∈ Ioo a b, (g b - g a) * (deriv f c) = (f b - f a) * (deriv g c) :=
id         └─┘            └───┘              └───┘  
src         └─┘                  └───┘                    └───┘
typ        └─┘            └───┘              └───┘  
doc          └─┘                     └───┘                       └───┘
513  exists_ratio_has_deriv_at_eq_ratio_slope f (deriv f) hab hfc
id   └──────────────────────────────────────┘   └───┘   └─┘ └─┘
src  └──────────────────────────────────────┘    └───┘
typ  └──────────────────────────────────────┘   └───┘   └─┘ └─┘
doc  └──────────────────────────────────────┘    └───┘
514    (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id         └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
src                        └───────────────┘    └───────────┘ └─────────┘    └──────────┘
typ        └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
515    g (deriv g) hgc (λ x hx, ((hgd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id       └───┘   └─┘     └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
src       └───┘                            └───────────────┘    └───────────┘ └─────────┘    └──────────┘
typ      └───┘   └─┘     └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
doc       └───┘
516  
517  /-- Lagrange's Mean Value Theorem, `deriv` version. -/
518  lemma exists_deriv_eq_slope : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
id                                     └─┘   └───┘               
src                                     └─┘     └───┘                     
typ                                    └─┘   └───┘               
doc                                      └─┘      └───┘
519  exists_has_deriv_at_eq_slope f (deriv f) hab hfc
id   └──────────────────────────┘   └───┘   └─┘ └─┘
src  └──────────────────────────┘    └───┘
typ  └──────────────────────────┘   └───┘   └─┘ └─┘
doc  └──────────────────────────┘    └───┘
520    (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id         └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
src                        └───────────────┘    └───────────┘ └─────────┘    └──────────┘
typ        └┘    └─┘  └┘ └───────────────┘    └───────────┘ └─────────┘ └┘ └──────────┘
521  
522  end interval
523  
524  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
525  of the real line. If `f` is differentiable on the interior of `D` and `C < f'`, then
526  `f` grows faster than `C * x` on `D`, i.e., `C * (y - x) < f y - f x` whenever `x, y ∈ D`,
527  `x < y`. -/
528  theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                        └─┘         └────┘           
src                                                       └─┘         └────┘            
typ                                                       └─┘         └────┘           
doc                                                                    └────┘
529    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
530    {C} (hf'_gt : ∀ x ∈ interior D, C < deriv f x) :
id                        └──────┘     └───┘  
src                        └──────┘       └───┘
typ                       └──────┘     └───┘  
doc                        └──────┘        └───┘
531    ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
id                              
src                                     
typ                             
532  begin
st   └─────
533    assume x y hx hy hxy,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
534    have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
id                 └─┘           └─────────────┘   └┘ └┘ └┘
src    └──────────┘└─┘     └───┘└─────────────┘└─┘    
typ    └──────────┘└─┘  └───┘└─────────────┘└─┘└┘└┘└┘
doc    └──────────┘└─┘      └───┘               └─┘    
txt    └──────────┘         └───┘               └─┘    
par    └──────────┘         └───┘               └─┘    
pid    └───────┘└─┘         └───┘               └─┘    
st   ────────────────────────┘└───────────────────────────────┘└─
535    have hxyD' : Ioo x y ⊆ interior D,
id                  └─┘     └──────┘ 
src    └───────────┘└─┘   └──────┘
typ    └───────────┘└─┘ └──────┘
doc    └───────────┘└─┘   └──────┘
txt    └───────────┘              
par    └───────────┘              
pid    └────────┘└─┘              
st   ──────────────────────────────────┘└─
536      from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id            └──────────────────┘  └─────────┘  └──────────┘ └─────────────────┘ └──┘
src      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘    
typ      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘└──┘
doc      └───┘                                └┘                                   
txt      └───┘                                └┘                                   
par      └───┘                                └┘                                   
pid      └───┘                                └┘                                   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
537    obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id                                  └─┘     └───┘                     
src    └──────────────────────┘└───┘└─┘  └───┘       └┘    
typ    └──────────────────────┘└───┘└─┘  └───┘      └┘  
doc    └──────────────────────┘ └───┘└─┘   └───┘         └┘     
txt    └──────────────────────┘ └───┘                    └┘     
par    └──────────────────────┘ └───┘                    └┘     
pid          └────────────────┘ └───┘                    └┘     
st   ─────────────────────────────────────────────────────────────────────────┘└─
538      from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
id            └───────────────────┘  └─┘  └─────┘ └──┘   └──────┘ └───┘
src      └───┘└───────────────────┘     └─────┘    └┘ └──────┘     
typ      └───┘└───────────────────┘└─┘ └─────┘└──┘└┘ └──────┘└───┘
doc      └───┘└───────────────────┘                └┘              
txt      └───┘                                     └┘              
par      └───┘                                     └┘              
pid      └───┘                                     └┘              
st   ───────────────────────────────────────────────────────────────────┘└─
539    have : C < (f y - f x) / (y - x), by { rw [← ha], exact hf'_gt _ (hxyD' a_mem) },
id                                             └┘         └────┘    └───┘ └───┘
src    └─────┘       └┘            └────┘    └────┘      └─┘           └┘
typ    └─────┘     └┘          └────┘└┘  └────┘└────┘└─┘ └───┘└───┘└┘
doc    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
txt    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
par    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
pid    └───┘└┘        └┘              └──┘               └─┘           
st   ─────────────────────────────────┘     └───────┘└──────────────────────────────┘└┘
540    exact (lt_div_iff (sub_pos.2 hxy)).1 this
id            └────────┘  └─────┘   └─┘     └──┘
src    └────┘ └────────┘ └─────┘└─┘   └───┘    
typ    └────┘ └────────┘ └─────┘└─┘└─┘└───┘└──┘
doc    └────┘                   └─┘   └───┘    
txt    └────┘                   └─┘   └───┘    
par    └────┘                   └─┘   └───┘    
pid                            └─┘   └───┘    
st   ───────────────────────────────────────────┘
541  end
st   └─┘
542  
543  /-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than
544  `C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`. -/
545  theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                            └────────────┘  
src                                                           └────────────┘ 
typ                                                           └────────────┘  
doc                                                             └────────────┘
546    {C} (hf'_gt : ∀ x, C < deriv f x) ⦃x y⦄ (hxy : x < y) :
id                         └───┘                   
src                          └───┘                     
typ                        └───┘                   
doc                           └───┘
547    C * (y - x) < f y - f x :=
id                 
src                   
typ                
548  convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuous_on hf.differentiable_on
id   └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src  └─────────┘└───────────────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ  └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc             └───────────────────────────────┘
549    (λ x _, hf'_gt x) x y trivial trivial hxy
id           └────┘     └─────┘ └─────┘ └─┘
src                          └─────┘ └─────┘
typ          └────┘     └─────┘ └─────┘ └─┘
550  
551  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
552  of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
553  `f` grows at least as fast as `C * x` on `D`, i.e., `C * (y - x) ≤ f y - f x` whenever `x, y ∈ D`,
554  `x ≤ y`. -/
555  theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                        └─┘         └────┘           
src                                                       └─┘         └────┘            
typ                                                       └─┘         └────┘           
doc                                                                    └────┘
556    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
557    {C} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) :
id                        └──────┘     └───┘  
src                        └──────┘       └───┘
typ                       └──────┘     └───┘  
doc                        └──────┘        └───┘
558    ∀ x y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x :=
id                              
src                                     
typ                             
559  begin
st   └─────
560    assume x y hx hy hxy,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
561    cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
id           └────────────┘ └─┘                        └──┘  └──────┘  └──────┘  └──────┘
src    └────┘└────────────┘   └─────────────┘     └──┘    └┘└──────┘└┘└──────┘└┘└──────┘
typ    └────┘└────────────┘└─┘└─────────────┘     └──┘└──┘└┘└──────┘└┘└──────┘└┘└──────┘
doc    └────┘                 └─────────────┘     └──┘    └┘        └┘        └┘        
txt    └────┘                 └─────────────┘     └──┘    └┘        └┘        └┘        
par    └────┘                 └─────────────┘     └──┘    └┘        └┘        └┘        
pid                          └─────────────┘       └┘    └┘        └┘        └┘        
st   ────────────────────────────────────────┘         └──┘└────────┘└────────┘└────────┘└─
562    have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
id                 └─┘           └─────────────┘   └┘ └┘ └┘
src    └──────────┘└─┘     └───┘└─────────────┘└─┘    
typ    └──────────┘└─┘  └───┘└─────────────┘└─┘└┘└┘└┘
doc    └──────────┘└─┘      └───┘               └─┘    
txt    └──────────┘         └───┘               └─┘    
par    └──────────┘         └───┘               └─┘    
pid    └───────┘└─┘         └───┘               └─┘    
st   ────────────────────────┘└───────────────────────────────┘└─
563    have hxyD' : Ioo x y ⊆ interior D,
id                  └─┘     └──────┘ 
src    └───────────┘└─┘   └──────┘
typ    └───────────┘└─┘ └──────┘
doc    └───────────┘└─┘   └──────┘
txt    └───────────┘              
par    └───────────┘              
pid    └────────┘└─┘              
st   ──────────────────────────────────┘└─
564      from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id            └──────────────────┘  └─────────┘  └──────────┘ └─────────────────┘ └──┘
src      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘    
typ      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘└──┘
doc      └───┘                                └┘                                   
txt      └───┘                                └┘                                   
par      └───┘                                └┘                                   
pid      └───┘                                └┘                                   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
565    obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id                                  └─┘     └───┘                     
src    └──────────────────────┘└───┘└─┘  └───┘       └┘    
typ    └──────────────────────┘└───┘└─┘  └───┘      └┘  
doc    └──────────────────────┘ └───┘└─┘   └───┘         └┘     
txt    └──────────────────────┘ └───┘                    └┘     
par    └──────────────────────┘ └───┘                    └┘     
pid          └────────────────┘ └───┘                    └┘     
st   ─────────────────────────────────────────────────────────────────────────┘└─
566      from exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD'),
id            └───────────────────┘  └──┘  └─────┘ └──┘   └──────┘ └───┘
src      └───┘└───────────────────┘      └─────┘    └┘ └──────┘     
typ      └───┘└───────────────────┘└──┘ └─────┘└──┘└┘ └──────┘└───┘
doc      └───┘└───────────────────┘                 └┘              
txt      └───┘                                      └┘              
par      └───┘                                      └┘              
pid      └───┘                                      └┘              
st   ────────────────────────────────────────────────────────────────────┘└─
567    have : C ≤ (f y - f x) / (y - x), by { rw [← ha], exact hf'_ge _ (hxyD' a_mem) },
id                                             └┘         └────┘    └───┘ └───┘
src    └─────┘       └┘            └────┘    └────┘      └─┘           └┘
typ    └─────┘     └┘          └────┘└┘  └────┘└────┘└─┘ └───┘└───┘└┘
doc    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
txt    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
par    └─────┘        └┘            └────┘    └────┘      └─┘           └┘
pid    └───┘└┘        └┘              └──┘               └─┘           
st   ─────────────────────────────────┘     └───────┘└──────────────────────────────┘└┘
568    exact (le_div_iff (sub_pos.2 hxy')).1 this
id            └────────┘  └─────┘   └──┘     └──┘
src    └────┘ └────────┘ └─────┘└─┘    └───┘    
typ    └────┘ └────────┘ └─────┘└─┘└──┘└───┘└──┘
doc    └────┘                   └─┘    └───┘    
txt    └────┘                   └─┘    └───┘    
par    └────┘                   └─┘    └───┘    
pid                            └─┘    └───┘    
st   ────────────────────────────────────────────┘
569  end
st   └─┘
570  
571  /-- Let `f : ℝ → ℝ` be a differentiable function. If `C ≤ f'`, then `f` grows at least as fast
572  as `C * x`, i.e., `C * (y - x) ≤ f y - f x` whenever `x ≤ y`. -/
573  theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                            └────────────┘  
src                                                           └────────────┘ 
typ                                                           └────────────┘  
doc                                                             └────────────┘
574    {C} (hf'_ge : ∀ x, C ≤ deriv f x) ⦃x y⦄ (hxy : x ≤ y) :
id                         └───┘                   
src                          └───┘                     
typ                        └───┘                   
doc                           └───┘
575    C * (y - x) ≤ f y - f x :=
id                 
src                   
typ                
576  convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuous_on hf.differentiable_on
id   └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src  └─────────┘└───────────────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ  └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc             └───────────────────────────────┘
577    (λ x _, hf'_ge x) x y trivial trivial hxy
id           └────┘     └─────┘ └─────┘ └─┘
src                          └─────┘ └─────┘
typ          └────┘     └─────┘ └─────┘ └─┘
578  
579  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
580  of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
581  `f` grows slower than `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x, y ∈ D`,
582  `x < y`. -/
583  theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                        └─┘         └────┘           
src                                                       └─┘         └────┘            
typ                                                       └─┘         └────┘           
doc                                                                    └────┘
584    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
585    {C} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) :
id                        └──────┘   └───┘    
src                        └──────┘    └───┘     
typ                       └──────┘   └───┘    
doc                        └──────┘    └───┘
586    ∀ x y ∈ D, x < y → f y - f x < C * (y - x) :=
id                             
src                                      
typ                            
587  begin
st   └─────
588    assume x y hx hy hxy,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
589    have hf'_gt : ∀ x ∈ interior D, -C < deriv (λ y, -f y) x,
id                         └──────┘     └───┘        
src    └────────────┘ └───┘└──────┘   └───┘  └──┘   └┘
typ    └────────────┘ └───┘└──────┘ └───┘  └──┘  └┘
doc    └────────────┘ └───┘└──────┘     └───┘  └──┘   └┘
txt    └────────────┘ └───┘                    └──┘   └┘
par    └────────────┘ └───┘                    └──┘   └┘
pid    └─────────┘└─┘ └───┘                    └──┘   └┘
st   ─────────────────────────────────────────────────────────┘└─
590    { assume x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
591      rw [deriv_neg, neg_lt_neg_iff],
id           └───────┘  └────────────┘
src      └──┘└───────┘└┘└────────────┘
typ      └──┘└───────┘└┘└────────────┘
doc      └──┘         └┘              
txt      └──┘         └┘              
par      └──┘         └┘              
pid        └┘         └┘              
st   ────────────────┘└──────────────┘└──
592      exact lt_hf' x hx },
id             └────┘  └┘
src      └────┘         
typ      └────┘└────┘└┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ─────────────────────┘└┘
593    simpa [-neg_lt_neg_iff]
src    └───────────────────────
typ    └───────────────────────
doc    └───────────────────────
txt    └───────────────────────
par    └───────────────────────
pid         └───────────────┘
st   ──────────────────────────
594      using neg_lt_neg (hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x y hx hy hxy)
id             └────────┘  └─────────────────────────────────┘ └────┘ └─────┘ └────┘   └┘ └┘ └─┘
src  ─────────┘└────────┘ └─────────────────────────────────┘└────┘└─────┘               └┘
typ  ─────────┘└────────┘ └─────────────────────────────────┘└────┘└─────┘└────┘└┘└┘└─┘└┘
doc  ─────────┘           └─────────────────────────────────┘                            └┘
txt  ─────────┘                                                                          └┘
par  ─────────┘                                                                          └┘
pid  ───┘└────┘                                                                          
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘
595  end
st   └─┘
596  
597  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
598  `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`. -/
599  theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                            └────────────┘  
src                                                           └────────────┘ 
typ                                                           └────────────┘  
doc                                                             └────────────┘
600    {C} (lt_hf' : ∀ x, deriv f x < C) ⦃x y⦄ (hxy : x < y) :
id                       └───┘                     
src                       └───┘                        
typ                      └───┘                     
doc                       └───┘
601    f y - f x < C * (y - x) :=
id                
src                    
typ               
602  convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuous_on hf.differentiable_on
id   └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src  └─────────┘└───────────────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ  └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc             └───────────────────────────────┘
603    (λ x _, lt_hf' x) x y trivial trivial hxy
id           └────┘     └─────┘ └─────┘ └─┘
src                          └─────┘ └─────┘
typ          └────┘     └─────┘ └─────┘ └─┘
604  
605  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
606  of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
607  `f` grows at most as fast as `C * x` on `D`, i.e., `f y - f x ≤ C * (y - x)` whenever `x, y ∈ D`,
608  `x ≤ y`. -/
609  theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                        └─┘         └────┘           
src                                                       └─┘         └────┘            
typ                                                       └─┘         └────┘           
doc                                                                    └────┘
610    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
611    {C} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) :
id                        └──────┘   └───┘    
src                        └──────┘    └───┘     
typ                       └──────┘   └───┘    
doc                        └──────┘    └───┘
612    ∀ x y ∈ D, x ≤ y → f y - f x ≤ C * (y - x) :=
id                             
src                                      
typ                            
613  begin
st   └─────
614    assume x y hx hy hxy,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
615    have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (λ y, -f y) x,
id                         └──────┘     └───┘        
src    └────────────┘ └───┘└──────┘   └───┘  └──┘   └┘
typ    └────────────┘ └───┘└──────┘ └───┘  └──┘  └┘
doc    └────────────┘ └───┘└──────┘     └───┘  └──┘   └┘
txt    └────────────┘ └───┘                    └──┘   └┘
par    └────────────┘ └───┘                    └──┘   └┘
pid    └─────────┘└─┘ └───┘                    └──┘   └┘
st   ─────────────────────────────────────────────────────────┘└─
616    { assume x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
617      rw [deriv_neg, neg_le_neg_iff],
id           └───────┘  └────────────┘
src      └──┘└───────┘└┘└────────────┘
typ      └──┘└───────┘└┘└────────────┘
doc      └──┘         └┘              
txt      └──┘         └┘              
par      └──┘         └┘              
pid        └┘         └┘              
st   ────────────────┘└──────────────┘└──
618      exact le_hf' x hx },
id             └────┘  └┘
src      └────┘         
typ      └────┘└────┘└┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ─────────────────────┘└┘
619    simpa [-neg_le_neg_iff]
src    └───────────────────────
typ    └───────────────────────
doc    └───────────────────────
txt    └───────────────────────
par    └───────────────────────
pid         └───────────────┘
st   ──────────────────────────
620      using neg_le_neg (hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x y hx hy hxy)
id             └────────┘  └─────────────────────────────────┘ └────┘ └─────┘ └────┘   └┘ └┘ └─┘
src  ─────────┘└────────┘ └─────────────────────────────────┘└────┘└─────┘               └┘
typ  ─────────┘└────────┘ └─────────────────────────────────┘└────┘└─────┘└────┘└┘└┘└─┘└┘
doc  ─────────┘           └─────────────────────────────────┘                            └┘
txt  ─────────┘                                                                          └┘
par  ─────────┘                                                                          └┘
pid  ───┘└────┘                                                                          
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘
621  end
st   └─┘
622  
623  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
624  as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`. -/
625  theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                            └────────────┘  
src                                                           └────────────┘ 
typ                                                           └────────────┘  
doc                                                             └────────────┘
626    {C} (le_hf' : ∀ x, deriv f x ≤ C) ⦃x y⦄ (hxy : x ≤ y) :
id                       └───┘                     
src                       └───┘                        
typ                      └───┘                     
doc                       └───┘
627    f y - f x ≤ C * (y - x) :=
id                
src                    
typ               
628  convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuous_on hf.differentiable_on
id   └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src  └─────────┘└───────────────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ  └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc             └───────────────────────────────┘
629    (λ x _, le_hf' x) x y trivial trivial hxy
id           └────┘     └─────┘ └─────┘ └─┘
src                          └─────┘ └─────┘
typ          └────┘     └─────┘ └─────┘ └─┘
630  
631  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
632  of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
633  `f` is a strictly monotonically increasing function on `D`. -/
634  theorem convex.strict_mono_of_deriv_pos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                └─┘         └────┘           
src                                               └─┘         └────┘            
typ                                               └─┘         └────┘           
doc                                                            └────┘
635    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
636    (hf'_pos : ∀ x ∈ interior D, 0 < deriv f x) :
id                     └──────┘      └───┘  
src                     └──────┘       └───┘
typ                    └──────┘      └───┘  
doc                     └──────┘        └───┘
637    ∀ x y ∈ D, x < y → f x < f y :=
id                      
src                          
typ                     
638  by simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf hf' hf'_pos
id                  └──────┘  └─────┘        └─────────────────────────────────┘ └┘ └─┘ └─────┘
src     └──────────┘└──────┘└┘└─────┘└──────┘└─────────────────────────────────┘            
typ     └──────────┘└──────┘└┘└─────┘└──────┘└─────────────────────────────────┘└┘└─┘└─────┘
doc     └──────────┘        └┘       └──────┘└─────────────────────────────────┘            
txt     └──────────┘        └┘       └──────┘                                               
par     └──────────┘        └┘       └──────┘                                               
pid          └──┘└┘        └┘       └────┘                                               
st     └────────────────────────────────────────────────────────────────────────────────────────
639  
src  
typ  
doc  
txt  
par  
pid  
st   
640  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
641  `f` is a strictly monotonically increasing function. -/
642  theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                    └────────────┘  
src                                                   └────────────┘ 
typ                                                   └────────────┘  
doc                                                     └────────────┘
643    (hf'_pos : ∀ x, 0 < deriv f x) :
id                       └───┘  
src                       └───┘
typ                      └───┘  
doc                        └───┘
644    strict_mono f :=
id     └─────────┘ 
src    └─────────┘
typ    └─────────┘ 
doc    └─────────┘
645  λ x y hxy, convex_univ.strict_mono_of_deriv_pos hf.continuous.continuous_on hf.differentiable_on
id       └─┘  └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src             └─────────┘└───────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ      └─┘  └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc                        └───────────────────────┘
646    (λ x _, hf'_pos x) x y trivial trivial hxy
id           └─────┘     └─────┘ └─────┘ └─┘
src                           └─────┘ └─────┘
typ          └─────┘     └─────┘ └─────┘ └─┘
647  
648  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
649  of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
650  `f` is a monotonically increasing function on `D`. -/
651  theorem convex.mono_of_deriv_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                            └─┘         └────┘           
src                                           └─┘         └────┘            
typ                                           └─┘         └────┘           
doc                                                        └────┘
652    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
653    (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
id                        └──────┘      └───┘  
src                        └──────┘       └───┘
typ                       └──────┘      └───┘  
doc                        └──────┘        └───┘
654    ∀ x y ∈ D, x ≤ y → f x ≤ f y :=
id                      
src                          
typ                     
655  by simpa only [zero_mul, sub_nonneg] using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg
id                  └──────┘  └────────┘        └─────────────────────────────────┘ └┘ └─┘ └────────┘
src     └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘               
typ     └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘└┘└─┘└────────┘
doc     └──────────┘        └┘          └──────┘└─────────────────────────────────┘               
txt     └──────────┘        └┘          └──────┘                                                  
par     └──────────┘        └┘          └──────┘                                                  
pid          └──┘└┘        └┘          └────┘                                                  
st     └──────────────────────────────────────────────────────────────────────────────────────────────
656  
src  
typ  
doc  
txt  
par  
pid  
st   
657  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
658  `f` is a monotonically increasing function. -/
659  theorem mono_of_deriv_nonneg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, 0 ≤ deriv f x) :
id                                                └────────────┘                  └───┘  
src                                               └────────────┘                    └───┘
typ                                               └────────────┘                  └───┘  
doc                                                 └────────────┘                      └───┘
660    monotone f :=
id     └──────┘ 
src    └──────┘
typ    └──────┘ 
doc    └──────┘
661  λ x y hxy, convex_univ.mono_of_deriv_nonneg hf.continuous.continuous_on hf.differentiable_on
id       └─┘  └─────────┘└───────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src             └─────────┘└───────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ      └─┘  └─────────┘└───────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc                        └───────────────────┘
662    (λ x _, hf' x) x y trivial trivial hxy
id           └─┘     └─────┘ └─────┘ └─┘
src                       └─────┘ └─────┘
typ          └─┘     └─────┘ └─────┘ └─┘
663  
664  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
665  of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
666  `f` is a strictly monotonically decreasing function on `D`. -/
667  theorem convex.strict_antimono_of_deriv_neg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                    └─┘         └────┘           
src                                                   └─┘         └────┘            
typ                                                   └─┘         └────┘           
doc                                                                └────┘
668    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
669    (hf'_neg : ∀ x ∈ interior D, deriv f x < 0) :
id                     └──────┘   └───┘   
src                     └──────┘    └───┘     
typ                    └──────┘   └───┘   
doc                     └──────┘    └───┘
670    ∀ x y ∈ D, x < y → f y < f x :=
id                      
src                          
typ                     
671  by simpa only [zero_mul, sub_lt_zero] using hD.image_sub_lt_mul_sub_of_deriv_lt hf hf' hf'_neg
id                  └──────┘  └─────────┘        └─────────────────────────────────┘ └┘ └─┘ └─────┘
src     └──────────┘└──────┘└┘└─────────┘└──────┘└─────────────────────────────────┘            
typ     └──────────┘└──────┘└┘└─────────┘└──────┘└─────────────────────────────────┘└┘└─┘└─────┘
doc     └──────────┘        └┘           └──────┘└─────────────────────────────────┘            
txt     └──────────┘        └┘           └──────┘                                               
par     └──────────┘        └┘           └──────┘                                               
pid          └──┘└┘        └┘           └────┘                                               
st     └────────────────────────────────────────────────────────────────────────────────────────────
672  
src  
typ  
doc  
txt  
par  
pid  
st   
673  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
674  `f` is a strictly monotonically decreasing function. -/
675  theorem strict_antimono_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                        └────────────┘  
src                                                       └────────────┘ 
typ                                                       └────────────┘  
doc                                                         └────────────┘
676    (hf' : ∀ x, deriv f x < 0) :
id                └───┘   
src                └───┘     
typ               └───┘   
doc                └───┘
677    ∀ ⦃x y⦄, x < y → f y < f x :=
id                     
src                        
typ                    
678  λ x y hxy, convex_univ.strict_antimono_of_deriv_neg hf.continuous.continuous_on hf.differentiable_on
id       └─┘  └─────────┘└───────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src             └─────────┘└───────────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ      └─┘  └─────────┘└───────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc                        └───────────────────────────┘
679    (λ x _, hf' x) x y trivial trivial hxy
id           └─┘     └─────┘ └─────┘ └─┘
src                       └─────┘ └─────┘
typ          └─┘     └─────┘ └─────┘ └─┘
680  
681  /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
682  of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
683  `f` is a monotonically decreasing function on `D`. -/
684  theorem convex.antimono_of_deriv_nonpos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                                └─┘         └────┘           
src                                               └─┘         └────┘            
typ                                               └─┘         └────┘           
doc                                                            └────┘
685    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
686    (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
id                        └──────┘   └───┘   
src                        └──────┘    └───┘     
typ                       └──────┘   └───┘   
doc                        └──────┘    └───┘
687    ∀ x y ∈ D, x ≤ y → f y ≤ f x :=
id                      
src                          
typ                     
688  by simpa only [zero_mul, sub_nonpos] using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos
id                  └──────┘  └────────┘        └─────────────────────────────────┘ └┘ └─┘ └────────┘
src     └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘               
typ     └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘└┘└─┘└────────┘
doc     └──────────┘        └┘          └──────┘└─────────────────────────────────┘               
txt     └──────────┘        └┘          └──────┘                                                  
par     └──────────┘        └┘          └──────┘                                                  
pid          └──┘└┘        └┘          └────┘                                                  
st     └──────────────────────────────────────────────────────────────────────────────────────────────
689  
src  
typ  
doc  
txt  
par  
pid  
st   
690  /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
691  `f` is a monotonically decreasing function. -/
692  theorem antimono_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, deriv f x ≤ 0) :
id                                                    └────────────┘               └───┘   
src                                                   └────────────┘                 └───┘     
typ                                                   └────────────┘               └───┘   
doc                                                     └────────────┘                  └───┘
693    ∀ ⦃x y⦄, x ≤ y → f y ≤ f x :=
id                     
src                        
typ                    
694  λ x y hxy, convex_univ.antimono_of_deriv_nonpos hf.continuous.continuous_on hf.differentiable_on
id       └─┘  └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src             └─────────┘└───────────────────────┘   └─────────┘└────────────┘   └────────────────┘
typ      └─┘  └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc                        └───────────────────────┘
695    (λ x _, hf' x) x y trivial trivial hxy
id           └─┘     └─────┘ └─────┘ └─┘
src                       └─────┘ └─────┘
typ          └─┘     └─────┘ └─────┘ └─┘
696  
697  /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
698  and `f'` is monotone on the interior, then `f` is convex on `D`. -/
699  theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                        └─┘         └────┘           
src                                       └─┘         └────┘            
typ                                       └─┘         └────┘           
doc                                                    └────┘
700    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
701    (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f x ≤ deriv f y) :
id                       └──────┘        └───┘    └───┘  
src                        └──────┘           └───┘      └───┘
typ                      └──────┘        └───┘    └───┘  
doc                        └──────┘            └───┘       └───┘
702    convex_on D f :=
id     └───────┘  
src    └───────┘
typ    └───────┘  
doc    └───────┘
703  convex_on_real_of_slope_mono_adjacent hD
id   └───────────────────────────────────┘ └┘
src  └───────────────────────────────────┘
typ  └───────────────────────────────────┘ └┘
doc  └───────────────────────────────────┘
704  begin
st   └─────
705    intros x y z hx hz hxy hyz,
src    └────────────────────────┘
typ    └────────────────────────┘
doc    └────────────────────────┘
txt    └────────────────────────┘
par    └────────────────────────┘
pid          └──────────────────┘
st   ───────────────────────────┘└─
706    -- First we prove some trivial inclusions
st   ────────────────────────────────────────────
707    have hxzD : Icc x z ⊆ D, from convex_real_iff.1 hD hx hz,
id                 └─┘           └─────────────┘   └┘ └┘ └┘
src    └──────────┘└─┘     └───┘└─────────────┘└─┘    
typ    └──────────┘└─┘  └───┘└─────────────┘└─┘└┘└┘└┘
doc    └──────────┘└─┘      └───┘               └─┘    
txt    └──────────┘         └───┘               └─┘    
par    └──────────┘         └───┘               └─┘    
pid    └───────┘└─┘         └───┘               └─┘    
st   ────────────────────────┘└───────────────────────────────┘└─
708    have hxyD : Icc x y ⊆ D, from subset.trans (Icc_subset_Icc_right $ le_of_lt hyz) hxzD,
id                 └─┘            └──────────┘  └──────────────────┘   └──────┘ └─┘  └──┘
src    └──────────┘└─┘      └───┘└──────────┘ └──────────────────┘ └──────┘   └┘
typ    └──────────┘└─┘   └───┘└──────────┘ └──────────────────┘ └──────┘└─┘└┘└──┘
doc    └──────────┘└─┘      └───┘                                             └┘
txt    └──────────┘         └───┘                                             └┘
par    └──────────┘         └───┘                                             └┘
pid    └───────┘└─┘         └───┘                                             └┘
st   ────────────────────────┘└────────────────────────────────────────────────────────────┘└─
709    have hxyD' : Ioo x y ⊆ interior D,
id                  └─┘     └──────┘ 
src    └───────────┘└─┘   └──────┘
typ    └───────────┘└─┘ └──────┘
doc    └───────────┘└─┘   └──────┘
txt    └───────────┘              
par    └───────────┘              
pid    └────────┘└─┘              
st   ──────────────────────────────────┘└─
710      from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id            └──────────────────┘  └─────────┘  └──────────┘ └─────────────────┘ └──┘
src      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘    
typ      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘└──┘
doc      └───┘                                └┘                                   
txt      └───┘                                └┘                                   
par      └───┘                                └┘                                   
pid      └───┘                                └┘                                   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
711    have hyzD : Icc y z ⊆ D, from subset.trans (Icc_subset_Icc_left $ le_of_lt hxy) hxzD,
id                 └─┘            └──────────┘  └─────────────────┘   └──────┘ └─┘  └──┘
src    └──────────┘└─┘      └───┘└──────────┘ └─────────────────┘ └──────┘   └┘
typ    └──────────┘└─┘   └───┘└──────────┘ └─────────────────┘ └──────┘└─┘└┘└──┘
doc    └──────────┘└─┘      └───┘                                            └┘
txt    └──────────┘         └───┘                                            └┘
par    └──────────┘         └───┘                                            └┘
pid    └───────┘└─┘         └───┘                                            └┘
st   ────────────────────────┘└───────────────────────────────────────────────────────────┘└─
712    have hyzD' : Ioo y z ⊆ interior D,
id                  └─┘     └──────┘ 
src    └───────────┘└─┘   └──────┘
typ    └───────────┘└─┘ └──────┘
doc    └───────────┘└─┘   └──────┘
txt    └───────────┘              
par    └───────────┘              
pid    └────────┘└─┘              
st   ──────────────────────────────────┘└─
713      from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hyzD⟩,
id            └──────────────────┘  └─────────┘  └──────────┘ └─────────────────┘ └──┘
src      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘    
typ      └───┘└──────────────────┘ └─────────┘└┘└──────────┘└─────────────────┘└──┘
doc      └───┘                                └┘                                   
txt      └───┘                                └┘                                   
par      └───┘                                └┘                                   
pid      └───┘                                └┘                                   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
714    -- Then we apply MVT to both `[x, y]` and `[y, z]`
st   ─────────────────────────────────────────────────────
715    obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id                                       └─┘     └───┘                     
src    └───────────────────────────┘└───┘└─┘  └───┘       └┘    
typ    └───────────────────────────┘└───┘└─┘  └───┘      └┘  
doc    └───────────────────────────┘ └───┘└─┘   └───┘         └┘     
txt    └───────────────────────────┘ └───┘                    └┘     
par    └───────────────────────────┘ └───┘                    └┘     
pid          └─────────────────────┘ └───┘                    └┘     
st   ──────────────────────────────────────────────────────────────────────────────┘└─
716      from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
id            └───────────────────┘  └─┘  └─────┘ └──┘   └──────┘ └───┘
src      └───┘└───────────────────┘     └─────┘    └┘ └──────┘     
typ      └───┘└───────────────────┘└─┘ └─────┘└──┘└┘ └──────┘└───┘
doc      └───┘└───────────────────┘                └┘              
txt      └───┘                                     └┘              
par      └───┘                                     └┘              
pid      └───┘                                     └┘              
st   ───────────────────────────────────────────────────────────────────┘└─
717    obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y),
id                                       └─┘     └───┘                        
src    └───────────────────────────┘└───┘└─┘  └───┘         └┘     
typ    └───────────────────────────┘└───┘└─┘  └───┘        └┘   
doc    └───────────────────────────┘ └───┘└─┘   └───┘         └┘     
txt    └───────────────────────────┘ └───┘                    └┘     
par    └───────────────────────────┘ └───┘                    └┘     
pid          └─────────────────────┘ └───┘                    └┘     
st   ──────────────────────────────────────────────────────────────────────────────┘└─
718      from exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD'),
id            └───────────────────┘  └─┘  └─────┘ └──┘   └──────┘ └───┘
src      └───┘└───────────────────┘     └─────┘    └┘ └──────┘     
typ      └───┘└───────────────────┘└─┘ └─────┘└──┘└┘ └──────┘└───┘
doc      └───┘└───────────────────┘                └┘              
txt      └───┘                                     └┘              
par      └───┘                                     └┘              
pid      └───┘                                     └┘              
st   ───────────────────────────────────────────────────────────────────┘└─
719    rw [← ha, ← hb],
id           └┘    └┘
src    └────┘  └──┘  
typ    └────┘└┘└──┘└┘
doc    └────┘  └──┘  
txt    └────┘  └──┘  
par    └────┘  └──┘  
pid      └──┘  └──┘  
st   ─────────┘└────┘└──
720    exact hf'_mono a b (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (le_of_lt $ lt_trans hay hyb)
id           └──────┘    └───┘  └─┘         └───┘       └─┘    └──────┘   └──────┘ └─┘ └─┘
src    └────┘                    └┘   └─┘          └┘   └─┘ └──────┘ └──────┘      └┘
typ    └────┘└──────┘ └───┘ └─┘└┘   └─┘ └───┘    └┘└─┘└─┘ └──────┘ └──────┘└─┘└─┘└┘
doc    └────┘                    └┘   └─┘          └┘   └─┘                        └┘
txt    └────┘                    └┘   └─┘          └┘   └─┘                        └┘
par    └────┘                    └┘   └─┘          └┘   └─┘                        └┘
pid                             └┘   └─┘          └┘   └─┘                        
st   ────────────────────────────────────────────────────────────────────────────────────────┘
721  end
st   └─┘
722  
723  /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
724  and `f'` is monotone on the interior, then `f` is convex on `ℝ`. -/
725  theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ f)
id                                                        └────────────┘  
src                                                       └────────────┘ 
typ                                                       └────────────┘  
doc                                                         └────────────┘
726    (hf'_mono : monotone (deriv f)) : convex_on univ f :=
id                 └──────┘  └───┘      └───────┘ └──┘ 
src                └──────┘  └───┘       └───────┘ └──┘
typ                └──────┘  └───┘      └───────┘ └──┘ 
doc                └──────┘  └───┘       └───────┘
727  convex_on_of_deriv_mono convex_univ hf.continuous.continuous_on hf.differentiable_on
id   └─────────────────────┘ └─────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src  └─────────────────────┘ └─────────┘   └─────────┘└────────────┘   └────────────────┘
typ  └─────────────────────┘ └─────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc  └─────────────────────┘
728    (λ x y _ _ h, hf'_mono h)
id              └──────┘ 
typ             └──────┘ 
729  
730  /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its interior,
731  and `f''` is nonnegative on the interior, then `f` is convex on `D`. -/
732  theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id                                           └─┘         └────┘           
src                                          └─┘         └────┘            
typ                                          └─┘         └────┘           
doc                                                       └────┘
733    (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id           └───────────┘           └───────────────┘    └──────┘ 
src          └───────────┘             └───────────────┘     └──────┘
typ          └───────────┘           └───────────────┘    └──────┘ 
doc          └───────────┘             └───────────────┘      └──────┘
734    (hf'' : differentiable_on ℝ (deriv f) (interior D))
id             └───────────────┘   └───┘    └──────┘ 
src            └───────────────┘   └───┘     └──────┘
typ            └───────────────┘   └───┘    └──────┘ 
doc            └───────────────┘    └───┘     └──────┘
735    (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ (deriv^[2] f x)) :
id                         └──────┘       └───┘└┘   
src                         └──────┘        └───┘└┘ 
typ                        └──────┘       └───┘└┘   
doc                         └──────┘         └───┘
736    convex_on D f :=
id     └───────┘  
src    └───────┘
typ    └───────┘  
doc    └───────┘
737  convex_on_of_deriv_mono hD hf hf' $
id   └─────────────────────┘ └┘ └┘ └─┘
src  └─────────────────────┘
typ  └─────────────────────┘ └┘ └┘ └─┘
doc  └─────────────────────┘
738  assume x y hx hy hxy,
id            └┘ └┘ └─┘
typ           └┘ └┘ └─┘
739  hD.interior.mono_of_deriv_nonneg hf''.continuous_on (by rwa [interior_interior])
id   └┘└───────┘└───────────────────┘ └──┘└────────────┘          └───────────────┘
src    └───────┘└───────────────────┘     └────────────┘     └───┘└───────────────┘
typ  └┘└───────┘└───────────────────┘ └──┘└────────────┘     └───┘└───────────────┘
doc    └───────┘└───────────────────┘                        └───┘                 
txt                                                          └───┘                 
par                                                          └───┘                 
pid                                                             └┘                 
st                                                          └─────────────────────┘
740    (by rwa [interior_interior]) _ _ hx hy hxy
id              └───────────────┘       └┘ └┘ └─┘
src        └───┘└───────────────┘
typ        └───┘└───────────────┘      └┘ └┘ └─┘
doc        └───┘                 
txt        └───┘                 
par        └───┘                 
pid           └┘                 
st        └─────────────────────┘
741  
742  /-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonnegative on `ℝ`,
743  then `f` is convex on `ℝ`. -/
744  theorem convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : differentiable ℝ f)
id                                                            └────────────┘  
src                                                           └────────────┘ 
typ                                                           └────────────┘  
doc                                                             └────────────┘
745    (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ x, 0 ≤ (deriv^[2] f x)) :
id             └────────────┘   └───┘                           └───┘└┘   
src            └────────────┘   └───┘                             └───┘└┘ 
typ            └────────────┘   └───┘                           └───┘└┘   
doc            └────────────┘    └───┘                              └───┘
746    convex_on univ f :=
id     └───────┘ └──┘ 
src    └───────┘ └──┘
typ    └───────┘ └──┘ 
doc    └───────┘
747  convex_on_of_deriv2_nonneg convex_univ hf'.continuous.continuous_on hf'.differentiable_on
id   └────────────────────────┘ └─────────┘ └─┘└─────────┘└────────────┘ └─┘└────────────────┘
src  └────────────────────────┘ └─────────┘    └─────────┘└────────────┘    └────────────────┘
typ  └────────────────────────┘ └─────────┘ └─┘└─────────┘└────────────┘ └─┘└────────────────┘
doc  └────────────────────────┘
748    hf''.differentiable_on (λ x _, hf''_nonneg x)
id     └──┘└────────────────┘       └─────────┘ 
src        └────────────────┘
typ    └──┘└────────────────┘       └─────────┘